perm filename XXXS.LIS[BMP,SYS] blob
sn#792081 filedate 1985-05-07 generic text, type C, neo UTF8
COMMENT ā VALID 00012 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 (PROVEALL '((BOOT-STRAP)) NIL "BOOT-STRAP")
C00003 00003 "PROVEALL"
C00113 00004 "RSA"
C00132 00005 "WILSON"
C00150 00006 "GAUSS"
C00213 00007 "FORTRAN"
C00228 00008 "CONTROLLER"
C00239 00009 "PR"
C00249 00010 "UNSOLV"
C00266 00011 "TMI"
C00285 00012 "ZTAK"
C00292 ENDMK
Cā;
(PROVEALL '((BOOT-STRAP)) NIL "BOOT-STRAP")
;;; "PROVEALL"
(PROVEALL
'((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
(PROVE-LEMMA PLUS-RIGHT-ID2 (REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (PLUS X Y)
(FIX X))))
(PROVE-LEMMA PLUS-ADD1 (REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X))))
(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE)
(EQUAL (PLUS X (PLUS Y Z))
(PLUS Y (PLUS X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z))))
(PROVE-LEMMA PLUS-EQUAL-0 (REWRITE)
(EQUAL (EQUAL (PLUS A B)
0)
(AND (ZEROP A)
(ZEROP B))))
(PROVE-LEMMA DIFFERENCE-X-X (REWRITE)
(EQUAL (DIFFERENCE X X) 0))
(PROVE-LEMMA DIFFERENCE-PLUS (REWRITE)
(AND (EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))))
(PROVE-LEMMA PLUS-CANCELLATION (REWRITE)
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B) (FIX C))))
(PROVE-LEMMA DIFFERENCE-0 (REWRITE)
(IMPLIES (NOT (LESSP Y X))
(EQUAL (DIFFERENCE X Y)
0)))
(PROVE-LEMMA EQUAL-DIFFERENCE-0 (REWRITE)
(EQUAL (EQUAL 0 (DIFFERENCE X Y))
(NOT (LESSP Y X))))
(PROVE-LEMMA DIFFERENCE-CANCELLATION-0 (REWRITE)
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X 0)
(ZEROP Y)))))
(PROVE-LEMMA DIFFERENCE-CANCELLATION-1 (REWRITE)
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z))))))
(DEFN APPEND (X Y)
(IF (LISTP X)
(CONS (CAR X)
(APPEND (CDR X)
Y))
Y))
(DEFN DELETE (X Y)
(IF (LISTP Y)
(IF (EQUAL X (CAR Y))
(CDR Y)
(CONS (CAR Y)
(DELETE X (CDR Y))))
Y))
(DEFN SUBBAGP (X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(SUBBAGP (CDR X)
(DELETE (CAR X)
Y))
F)
T))
(DEFN BAGDIFF (X Y)
(IF (LISTP Y)
(IF (MEMBER (CAR Y)
X)
(BAGDIFF (DELETE (CAR Y)
X)
(CDR Y))
(BAGDIFF X (CDR Y)))
X))
(DEFN BAGINT (X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(CONS (CAR X)
(BAGINT (CDR X)
(DELETE (CAR X)
Y)))
(BAGINT (CDR X)
Y))
NIL))
(PROVE-LEMMA DELETE-NON-MEMBER (REWRITE)
(IMPLIES (NOT (MEMBER X Y))
(EQUAL (DELETE X Y)
Y)))
(PROVE-LEMMA MEMBER-DELETE (REWRITE)
(IMPLIES (MEMBER X (DELETE U V))
(MEMBER X V)))
(PROVE-LEMMA COMMUTATIVITY-OF-DELETE (REWRITE)
(EQUAL (DELETE X (DELETE Y Z))
(DELETE Y (DELETE X Z))))
(PROVE-LEMMA SUBBAGP-DELETE (REWRITE)
(IMPLIES (SUBBAGP X (DELETE U Y))
(SUBBAGP X Y)))
(PROVE-LEMMA SUBBAGP-CDR1 (REWRITE)
(IMPLIES (SUBBAGP X Y)
(SUBBAGP (CDR X)
Y)))
(PROVE-LEMMA SUBBAGP-CDR2 (REWRITE)
(IMPLIES (SUBBAGP X (CDR Y))
(SUBBAGP X Y)))
(PROVE-LEMMA SUBBAGP-BAGINT1 (REWRITE)
(SUBBAGP (BAGINT X Y)
X))
(PROVE-LEMMA SUBBAGP-BAGINT2 (REWRITE)
(SUBBAGP (BAGINT X Y)
Y))
(DEFN PLUS-FRINGE (X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE PLUS)))
(APPEND (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X)))
(CONS X NIL)))
(DEFN PLUS-TREE (L)
(IF (NLISTP L)
(QUOTE (QUOTE 0))
(IF (NLISTP (CDR L))
(LIST (QUOTE FIX)
(CAR L))
(IF (NLISTP (CDDR L))
(LIST (QUOTE PLUS)
(CAR L)
(CADR L))
(LIST (QUOTE PLUS)
(CAR L)
(PLUS-TREE (CDR L)))))))
(DEFN
CANCEL
(X)
(IF
(AND (LISTP X)
(EQUAL (CAR X)
(QUOTE EQUAL)))
(IF
(AND (LISTP (CADR X))
(EQUAL (CAADR X)
(QUOTE PLUS))
(LISTP (CADDR X))
(EQUAL (CAADDR X)
(QUOTE PLUS)))
(LIST (QUOTE EQUAL)
(PLUS-TREE (BAGDIFF
(PLUS-FRINGE (CADR X))
(BAGINT (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X)))))
(PLUS-TREE (BAGDIFF
(PLUS-FRINGE (CADDR X))
(BAGINT (PLUS-FRINGE (CADR X))
(PLUS-FRINGE (CADDR X))))))
(IF
(AND (LISTP (CADR X))
(EQUAL (CAADR X)
(QUOTE PLUS))
(MEMBER (CADDR X)
(PLUS-FRINGE (CADR X))))
(LIST (QUOTE IF)
(LIST (QUOTE NUMBERP)
(CADDR X))
(LIST (QUOTE EQUAL)
(PLUS-TREE (DELETE
(CADDR X)
(PLUS-FRINGE (CADR X))))
(QUOTE (QUOTE 0)))
(LIST (QUOTE QUOTE)
F))
(IF
(AND (LISTP (CADDR X))
(EQUAL (CAADDR X)
(QUOTE PLUS))
(MEMBER (CADR X)
(PLUS-FRINGE (CADDR X))))
(LIST (QUOTE IF)
(LIST (QUOTE NUMBERP)
(CADR X))
(LIST (QUOTE EQUAL)
(QUOTE (QUOTE 0))
(PLUS-TREE
(DELETE (CADR X)
(PLUS-FRINGE (CADDR X)))))
(LIST (QUOTE QUOTE)
F))
X)))
X))
(PROVE-LEMMA FORM-LSTP-APPEND (REWRITE)
(IMPLIES (AND (FORM-LSTP A)
(FORM-LSTP B))
(FORM-LSTP (APPEND A B))))
(PROVE-LEMMA FORM-LSTP-PLUS-FRINGE (REWRITE)
(IMPLIES (FORMP X)
(FORM-LSTP (PLUS-FRINGE X))))
(PROVE-LEMMA FORM-LSTP-DELETE (REWRITE)
(IMPLIES (FORM-LSTP X)
(FORM-LSTP (DELETE Y X))))
(PROVE-LEMMA FORM-LSTP-BAGDIFF (REWRITE)
(IMPLIES (FORM-LSTP X)
(FORM-LSTP (BAGDIFF X Y))))
(PROVE-LEMMA FORMP-PLUS-TREE (REWRITE)
(IMPLIES (FORM-LSTP X)
(FORMP (PLUS-TREE X))))
(PROVE-LEMMA NUMBERP-MEANING-PLUS (REWRITE)
(IMPLIES (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE PLUS)))
(NUMBERP (MEANING X A))))
(PROVE-LEMMA NUMBERP-MEANING-PLUS-TREE (REWRITE)
(NUMBERP (MEANING (PLUS-TREE L)
A)))
(PROVE-LEMMA MEMBER-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE)
(IMPLIES (MEMBER X Y)
(NOT (LESSP (MEANING (PLUS-TREE Y)
A)
(MEANING X A)))))
(PROVE-LEMMA PLUS-TREE-DELETE (REWRITE)
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A))))
(PROVE-LEMMA SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE)
(IMPLIES (SUBBAGP X Y)
(NOT (LESSP (MEANING (PLUS-TREE Y)
A)
(MEANING (PLUS-TREE X)
A)))))
(PROVE-LEMMA PLUS-TREE-BAGDIFF (REWRITE)
(IMPLIES (SUBBAGP X Y)
(EQUAL (MEANING
(PLUS-TREE (BAGDIFF Y X))
A)
(DIFFERENCE
(MEANING (PLUS-TREE Y)
A)
(MEANING (PLUS-TREE X)
A)))))
(PROVE-LEMMA NUMBERP-MEANING-BRIDGE (REWRITE)
(IMPLIES (EQUAL (MEANING Z A)
(MEANING (PLUS-TREE X)
A))
(NUMBERP (MEANING Z A))))
(PROVE-LEMMA
BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP
(REWRITE)
(IMPLIES (AND (SUBBAGP Y (PLUS-FRINGE Z))
(EQUAL (MEANING Z A)
(MEANING (PLUS-TREE (PLUS-FRINGE Z))
A)))
(EQUAL (LESSP (MEANING Z A)
(MEANING (PLUS-TREE Y)
A))
F))
; These bridge lemmas are needed because we are soon to prove that MEANING of
; (PLUS-TREE (PLUS-FRINGE X)) is MEANING of X. Thus, such facts that the
; MEANING of the PLUS-TREE of the PLUS-FRINGE is greater than or equal to
; that of the intersection -- which follows from
; SUBGAGP-IMPLIES-PLUS-TREE-GREATEREQP -- get covered up. You will note that
; in a hand proof of the CANCEL lemma, we do all the arithmetic and such with
; the PLUS-TREE of the PLUS-FRINGE, and only at the very end rewrite that to
; the original arg.
)
(PROVE-LEMMA MEANING-PLUS-TREE-APPEND (REWRITE)
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A))))
(PROVE-LEMMA PLUS-TREE-PLUS-FRINGE (REWRITE)
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A))))
(PROVE-LEMMA MEMBER-IMPLIES-NUMBERP (REWRITE)
(IMPLIES (AND (MEMBER C (PLUS-FRINGE X))
(NUMBERP (MEANING C A)))
(NUMBERP (MEANING X A))))
(PROVE-LEMMA CORRECTNESS-OF-CANCEL ((META EQUAL))
(IMPLIES (FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (CANCEL X)
A))
(FORMP (CANCEL X)))))
(DEFN REVERSE (X)
(IF (LISTP X)
(APPEND (REVERSE (CDR X))
(CONS (CAR X)
NIL))
NIL))
(PROVE-LEMMA ASSOCIATIVITY-OF-APPEND (REWRITE)
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z))))
(DEFN PLISTP (X)
(IF (LISTP X)
(PLISTP (CDR X))
(EQUAL X NIL)))
(PROVE-LEMMA APPEND-RIGHT-ID (REWRITE)
(IMPLIES (PLISTP X)
(EQUAL (APPEND X NIL)
X)))
(PROVE-LEMMA PLISTP-REVERSE (GENERALIZE REWRITE)
(PLISTP (REVERSE X)))
(PROVE-LEMMA APPEND-REVERSE (REWRITE)
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A))))
(PROVE-LEMMA TIMES-ZERO2 (REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X Y)
0)))
(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (REWRITE)
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z))))
(PROVE-LEMMA TIMES-ADD1 (REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X))))
(PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE)
(EQUAL (TIMES X Y)
(TIMES Y X)))
(PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE)
(EQUAL (TIMES X (TIMES Y Z))
(TIMES Y (TIMES X Z))))
(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE)
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z))))
(PROVE-LEMMA EQUAL-TIMES-0 (REWRITE)
(EQUAL (EQUAL (TIMES X Y)
0)
(OR (ZEROP X)
(ZEROP Y))))
(ADD-SHELL PUSH NIL STACKP ((TOP (NONE-OF)
ZERO)
(POP (NONE-OF)
ZERO)))
(DCL CALL (FN X Y))
(DCL GETVALUE (VAR ENVRN))
(ADD-AXIOM NUMBERP-CALL (REWRITE)
(NUMBERP (CALL FN X Y)))
(DEFN
EXPRESSIONP
(X)
(IF (LISTP X)
(IF (LISTP (CAR X))
F
(IF (LISTP (CDR X))
(IF (LISTP (CDDR X))
(IF (EXPRESSIONP (CADR X))
(EXPRESSIONP (CADDR X))
F)
F)
F))
T))
(PROVE-LEMMA CADR-CROCK (REWRITE)
(IMPLIES (LISTP (CDDR X))
(LESSP (COUNT (CADR X))
(COUNT X)))
; This is trivial by CAR/CDR-ELIM. However, in DEFN, when trying to prove
; the lemmas that justify recursion, we use only SIMPLIFY. So we have to
; prove this first.
)
(DEFN EVAL (FORM ENVRN)
(IF (NUMBERP FORM)
FORM
(IF (LISTP (CDDR FORM))
(CALL (CAR FORM)
(EVAL (CADR FORM)
ENVRN)
(EVAL (CADDR FORM)
ENVRN))
(GETVALUE FORM ENVRN))))
(DEFN OPTIMIZE (FORM)
(IF (LISTP (CDDR FORM))
(IF (NUMBERP (OPTIMIZE (CADR FORM)))
(IF (NUMBERP (OPTIMIZE (CADDR FORM)))
(CALL (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM)))
(LIST (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM))))
(LIST (CAR FORM)
(OPTIMIZE (CADR FORM))
(OPTIMIZE (CADDR FORM))))
FORM))
(DEFN CODEGEN (FORM INS)
(IF (NUMBERP FORM)
(CONS (LIST (QUOTE PUSHI)
FORM)
INS)
(IF (LISTP (CDDR FORM))
(CONS (CAR FORM)
(CODEGEN (CADDR FORM)
(CODEGEN (CADR FORM)
INS)))
(CONS (LIST (QUOTE PUSHV)
FORM)
INS))))
(DEFN COMPILE (FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
NIL)))
(PROVE-LEMMA FORMP-OPTIMIZE (REWRITE)
(IMPLIES (EXPRESSIONP X)
(EXPRESSIONP (OPTIMIZE X))))
(PROVE-LEMMA CORRECTNESS-OF-OPTIMIZE (REWRITE)
(IMPLIES (EXPRESSIONP X)
(EQUAL (EVAL (OPTIMIZE X)
ENVRN)
(EVAL X ENVRN))))
(DEFN
EXEC
(PC PDS ENVRN)
(IF (NLISTP PC)
PDS
(IF (LISTP (CAR PC))
(IF (EQUAL (CAAR PC)
(QUOTE PUSHI))
(EXEC (CDR PC)
(PUSH (CADAR PC)
PDS)
ENVRN)
(EXEC (CDR PC)
(PUSH (GETVALUE (CADAR PC)
ENVRN)
PDS)
ENVRN))
(EXEC (CDR PC)
(PUSH (CALL (CAR PC)
(TOP (POP PDS))
(TOP PDS))
(POP (POP PDS)))
ENVRN))))
(PROVE-LEMMA SEQUENTIAL-EXECUTION (REWRITE)
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN)))
(PROVE-LEMMA CORRECTNESS-OF-CODEGEN (REWRITE)
(IMPLIES (EXPRESSIONP X)
(EQUAL (EXEC (REVERSE (CODEGEN X INS))
PDS ENVRN)
(PUSH (EVAL X ENVRN)
(EXEC (REVERSE INS)
PDS ENVRN)))))
(PROVE-LEMMA CORRECTNESS-OF-OPTIMIZING-COMPILER NIL
(IMPLIES (EXPRESSIONP X)
(EQUAL (EXEC (COMPILE X)
PDS ENVRN)
(PUSH (EVAL X ENVRN)
PDS))))
(PROVE-LEMMA TRANSITIVITY-OF-LESSP NIL
(IMPLIES (AND (LESSP X Y)
(LESSP Y Z))
(LESSP X Z)))
(PROVE-LEMMA LESSP-NOT-REFLEXIVE NIL (NOT (LESSP X X)))
(DEFN EQP (X Y)
(EQUAL (FIX X)
(FIX Y)))
(PROVE-LEMMA TRICHOTOMY-OF-LESSP NIL
(IMPLIES (AND (NOT (EQP X Y))
(NOT (LESSP Y X)))
(LESSP X Y)))
(PROVE-LEMMA REVERSE-REVERSE (REWRITE)
(IMPLIES (PLISTP X)
(EQUAL (REVERSE (REVERSE X))
X)))
(DEFN FLATTEN (X)
(IF (LISTP X)
(APPEND (FLATTEN (CAR X))
(FLATTEN (CDR X)))
(CONS X NIL)))
(DEFN MC-FLATTEN (X Y)
(IF (LISTP X)
(MC-FLATTEN (CAR X)
(MC-FLATTEN (CDR X)
Y))
(CONS X Y)))
(PROVE-LEMMA FLATTEN-MC-FLATTEN (REWRITE)
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y)))
(PROVE-LEMMA MEMBER-APPEND (REWRITE)
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B))))
(PROVE-LEMMA MEMBER-REVERSE (REWRITE)
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y)))
(PROVE-LEMMA LENGTH-REVERSE (REWRITE)
(EQUAL (LENGTH (REVERSE X))
(LENGTH X)))
(DEFN INTERSECT (X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(CONS (CAR X)
(INTERSECT (CDR X)
Y))
(INTERSECT (CDR X)
Y))
NIL))
(PROVE-LEMMA MEMBER-INTERSECT (REWRITE)
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C))))
(DEFN UNION (X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X)
Y)
(UNION (CDR X)
Y)
(CONS (CAR X)
(UNION (CDR X)
Y)))
Y))
(PROVE-LEMMA MEMBER-UNION NIL (EQUAL (MEMBER A (UNION B C))
(OR (MEMBER A B)
(MEMBER A C))))
(PROVE-LEMMA SUBSETP-UNION NIL (IMPLIES (SUBSETP A B)
(EQUAL (UNION A B)
B)))
(PROVE-LEMMA SUBSETP-INTERSECT NIL
(IMPLIES (AND (PLISTP A)
(SUBSETP A B))
(EQUAL (INTERSECT A B)
A)))
(DEFN NTH (X N)
(IF (ZEROP N)
X
(NTH (CDR X)
(SUB1 N))))
(DEFN GREATEREQP (X Y)
(NOT (LESSP X Y)))
(PROVE-LEMMA TRANSITIVITY-OF-LEQ NIL (IMPLIES (AND (LEQ X Y)
(LEQ Y Z))
(LEQ X Z)))
(DEFN ORDERED (L)
(IF (LISTP L)
(IF (LISTP (CDR L))
(IF (LESSP (CADR L)
(CAR L))
F
(ORDERED (CDR L)))
T)
T))
(DEFN ADDTOLIST (X L)
(IF (LISTP L)
(IF (LESSP X (CAR L))
(CONS X L)
(CONS (CAR L)
(ADDTOLIST X (CDR L))))
(CONS X NIL)))
(DEFN SORT (L)
(IF (LISTP L)
(ADDTOLIST (CAR L)
(SORT (CDR L)))
NIL))
(DEFN ASSOC (X Y)
(IF (LISTP Y)
(IF (EQUAL X (CAAR Y))
(CAR Y)
(ASSOC X (CDR Y)))
NIL))
(DEFN BOOLEAN (X)
(OR (EQUAL X T)
(EQUAL X F)))
(DEFN IFF (X Y)
(AND
(IMPLIES X Y)
(IMPLIES Y X)))
(PROVE-LEMMA IFF-EQUAL-EQUAL NIL (IMPLIES (AND (BOOLEAN P)
(BOOLEAN Q))
(EQUAL (IFF P Q)
(EQUAL P Q))))
(PROVE-LEMMA NTH-0 (REWRITE)
(EQUAL (NTH 0 I)
0))
(PROVE-LEMMA NTH-NIL (REWRITE)
(EQUAL (NTH NIL I)
(IF (ZEROP I)
NIL 0)))
(PROVE-LEMMA NTH-APPEND1 (REWRITE)
(EQUAL (NTH A (PLUS I J))
(NTH (NTH A I)
J)))
(PROVE-LEMMA ASSOCIATIVITY-OF-EQUAL NIL
(IMPLIES (AND (BOOLEAN A)
(AND (BOOLEAN B)
(BOOLEAN C)))
(EQUAL (EQUAL (EQUAL A B)
C)
(EQUAL A (EQUAL B C)))))
(DEFN ODD (X)
(IF (ZEROP X)
F
(IF (ZEROP (SUB1 X))
T
(ODD (SUB1 (SUB1 X))))))
(DEFN EVEN1 (X)
(IF (ZEROP X)
T
(ODD (SUB1 X))))
(DEFN EVEN2 (X)
(IF (ZEROP X)
T
(IF (ZEROP (SUB1 X))
F
(EVEN2 (SUB1 (SUB1 X))))))
(DEFN DOUBLE (I)
(IF (ZEROP I)
0
(ADD1 (ADD1 (DOUBLE (SUB1 I))))))
(PROVE-LEMMA EVEN1-DOUBLE (REWRITE)
(EVEN1 (DOUBLE I)))
(DEFN HALF (I)
(IF (ZEROP I)
0
(IF (ZEROP (SUB1 I))
0
(ADD1 (HALF (SUB1 (SUB1 I)))))))
(PROVE-LEMMA HALF-DOUBLE (REWRITE)
(IMPLIES (NUMBERP I)
(EQUAL (HALF (DOUBLE I))
I)))
(PROVE-LEMMA DOUBLE-HALF (REWRITE)
(IMPLIES (AND (NUMBERP I)
(EVEN1 I))
(EQUAL (DOUBLE (HALF I))
I)))
(PROVE-LEMMA DOUBLE-TIMES-2 NIL (EQUAL (DOUBLE I)
(TIMES 2 I)))
(PROVE-LEMMA SUBSETP-CONS (REWRITE)
(IMPLIES (SUBSETP X Y)
(SUBSETP X (CONS Z Y))))
(PROVE-LEMMA LAST-APPEND (REWRITE)
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B))))
(PROVE-LEMMA LAST-REVERSE NIL
(IMPLIES (LISTP A)
(EQUAL (LAST (REVERSE A))
(CONS (CAR A)
NIL))))
(DEFN EXP (I J)
(IF (ZEROP J)
1
(TIMES I (EXP I (SUB1 J)))))
(PROVE-LEMMA EXP-PLUS (REWRITE)
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K))))
(PROVE-LEMMA EVEN1-EVEN2 NIL (EQUAL (EVEN1 X)
(EVEN2 X)))
(PROVE-LEMMA LEQ-NTH NIL (LEQ (LENGTH (NTH L I))
(LENGTH L)))
(PROVE-LEMMA MEMBER-SORT NIL (EQUAL (MEMBER A (SORT B))
(MEMBER A B)))
(PROVE-LEMMA LENGTH-SORT NIL (EQUAL (LENGTH (SORT A))
(LENGTH A)))
(DEFN COUNT-LIST (A L)
(IF (LISTP L)
(IF (EQUAL A (CAR L))
(ADD1 (COUNT-LIST A (CDR L)))
(COUNT-LIST A (CDR L)))
0))
(PROVE-LEMMA COUNT-LIST-SORT NIL
(EQUAL (COUNT-LIST A (SORT L))
(COUNT-LIST A L)))
(PROVE-LEMMA ORDERED-APPEND NIL (IMPLIES
(ORDERED (APPEND A B))
(ORDERED A)))
(PROVE-LEMMA LEQ-HALF NIL (LEQ (HALF I)
I))
(DEFN NUMBER-LISTP (L)
(IF (LISTP L)
(IF (NUMBERP (CAR L))
(NUMBER-LISTP (CDR L))
F)
(EQUAL L NIL)))
(PROVE-LEMMA ORDERED-SORT (REWRITE)
(ORDERED (SORT X)))
(PROVE-LEMMA ADDTOLIST-OF-ORDERED-NUMBER-LIST (REWRITE)
(IMPLIES (AND (ORDERED X)
(NUMBER-LISTP X)
(NUMBERP I)
(NOT (LESSP (CAR X)
I)))
(EQUAL (ADDTOLIST I X)
(CONS I X))))
(PROVE-LEMMA SORT-OF-ORDERED-NUMBER-LIST (REWRITE)
(IMPLIES (AND (ORDERED X)
(NUMBER-LISTP X))
(EQUAL (SORT X)
X)))
(DEFN XOR (P Q)
(IF Q (IF P F T)
(EQUAL P T)))
(PROVE-LEMMA CROCK-DUE-TO-LACK-OF-BOUNCE (REWRITE)
(IMPLIES (EQUAL X (SORT L))
(ORDERED X)))
(PROVE-LEMMA SORT-ORDERED (REWRITE)
(IMPLIES (NUMBER-LISTP L)
(EQUAL (EQUAL (SORT L)
L)
(ORDERED L))))
(DEFN SUBST (X Y Z)
(IF (EQUAL Y Z)
X
(IF (LISTP Z)
(CONS (SUBST X Y (CAR Z))
(SUBST X Y (CDR Z)))
Z)))
(PROVE-LEMMA SUBST-A-A NIL (EQUAL (SUBST A A B)
B))
(DEFN OCCUR (X Y)
(IF (EQUAL X Y)
T
(IF (LISTP Y)
(IF (OCCUR X (CAR Y))
T
(OCCUR X (CDR Y)))
F)))
(PROVE-LEMMA OCCUR-SUBST NIL (IMPLIES (NOT (OCCUR A B))
(EQUAL (SUBST C A B)
B)))
(DEFN COUNTPS-LOOP (L PRED ANS)
(IF (LISTP L)
(IF (CALL PRED (CAR L)
NIL)
(COUNTPS-LOOP (CDR L)
PRED
(ADD1 ANS))
(COUNTPS-LOOP (CDR L)
PRED ANS))
ANS))
(DEFN COUNTPS- (L PRED)
(COUNTPS-LOOP L PRED 0))
(DEFN COUNTPS (L PRED)
(IF (LISTP L)
(IF (CALL PRED (CAR L)
NIL)
(ADD1 (COUNTPS (CDR L)
PRED))
(COUNTPS (CDR L)
PRED))
0))
(PROVE-LEMMA COUNTPS-COUNTPS (REWRITE)
(IMPLIES (NUMBERP N)
(EQUAL (COUNTPS-LOOP L PRED N)
(PLUS N (COUNTPS L PRED)))))
(DEFN FACT (I)
(IF (ZEROP I)
1
(TIMES I (FACT (SUB1 I)))))
(DEFN FACT-LOOP (I ANS)
(IF (ZEROP I)
ANS
(FACT-LOOP (SUB1 I)
(TIMES I ANS))))
(DEFN FACT- (I)
(FACT-LOOP I 1))
(PROVE-LEMMA FACT-LOOP-FACT (REWRITE)
(IMPLIES (NUMBERP I)
(EQUAL (FACT-LOOP J I)
(TIMES I (FACT J)))))
(PROVE-LEMMA FACT-FACT NIL (EQUAL (FACT- I)
(FACT I)))
(DEFN REVERSE-LOOP (X ANS)
(IF (LISTP X)
(REVERSE-LOOP (CDR X)
(CONS (CAR X)
ANS))
ANS))
(DEFN REVERSE- (X)
(REVERSE-LOOP X NIL))
(PROVE-LEMMA REVERSE-LOOP-APPEND-REVERSE (REWRITE)
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y)))
(PROVE-LEMMA REVERSE-LOOP-REVERSE (REWRITE)
(EQUAL (REVERSE-LOOP X NIL)
(REVERSE X)))
(PROVE-LEMMA REVERSE-APPEND NIL (EQUAL (REVERSE- (APPEND A B))
(APPEND (REVERSE- B)
(REVERSE- A))))
(PROVE-LEMMA REVERSE-REVERSE- NIL
(IMPLIES (PLISTP X)
(EQUAL (REVERSE- (REVERSE- X))
X)))
(DEFN SORT-LP (X Y)
(IF (LISTP X)
(SORT-LP (CDR X)
(ADDTOLIST (CAR X)
Y))
Y))
(PROVE-LEMMA ORDERED-ADDTOLIST (REWRITE)
(IMPLIES (ORDERED Y)
(ORDERED (ADDTOLIST X Y))))
(PROVE-LEMMA ORDERED-SORT-LP (REWRITE)
(IMPLIES (ORDERED Y)
(ORDERED (SORT-LP X Y))))
(PROVE-LEMMA COUNT-SORT-LP (REWRITE)
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y))))
(PROVE-LEMMA APPEND-CANCELLATION (REWRITE)
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C)))
(PROVE-LEMMA EQUAL-LESSP (REWRITE)
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z))))
(PROVE-LEMMA DIFFERENCE-ELIM (ELIM)
(IMPLIES (AND (NUMBERP Y)
(NOT (LESSP Y X)))
(EQUAL (PLUS X (DIFFERENCE Y X))
Y)))
(DEFN POWER-EVAL (L BASE)
(IF (LISTP L)
(PLUS (CAR L)
(TIMES BASE (POWER-EVAL (CDR L)
BASE)))
0))
(DEFN BIG-PLUS1 (L I BASE)
(IF (LISTP L)
(IF (ZEROP I)
L
(CONS (REMAINDER (PLUS (CAR L)
I)
BASE)
(BIG-PLUS1 (CDR L)
(QUOTIENT (PLUS (CAR L)
I)
BASE)
BASE)))
(CONS I NIL)))
(PROVE-LEMMA REMAINDER-QUOTIENT (REWRITE)
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X)))
(PROVE-LEMMA POWER-EVAL-BIG-PLUS1 (REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I)))
(DEFN
BIG-PLUS
(X Y I BASE)
(IF (LISTP X)
(IF (LISTP Y)
(CONS (REMAINDER (PLUS I (PLUS (CAR X)
(CAR Y)))
BASE)
(BIG-PLUS (CDR X)
(CDR Y)
(QUOTIENT (PLUS I (PLUS (CAR X)
(CAR Y)))
BASE)
BASE))
(BIG-PLUS1 X I BASE))
(BIG-PLUS1 Y I BASE)))
(PROVE-LEMMA POWER-EVAL-BIG-PLUS (REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE)))))
(PROVE-LEMMA REMAINDER-WRT-1 (REWRITE)
(EQUAL (REMAINDER Y 1)
0))
(PROVE-LEMMA REMAINDER-WRT-12 (REWRITE)
(IMPLIES (NOT (NUMBERP X))
(EQUAL (REMAINDER Y X)
(FIX Y))))
(PROVE-LEMMA LESSP-REMAINDER2 (REWRITE GENERALIZE)
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y))))
(PROVE-LEMMA REMAINDER-X-X (REWRITE)
(EQUAL (REMAINDER X X)
0))
(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM (ELIM)
(IMPLIES (AND (NOT (ZEROP Y))
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)))
(PROVE-LEMMA LESSP-TIMES-1 (REWRITE)
(IMPLIES (NOT (ZEROP I))
(NOT (LESSP (TIMES I J)
J))))
(PROVE-LEMMA LESSP-TIMES-2 (REWRITE)
(IMPLIES (NOT (ZEROP I))
(NOT (LESSP (TIMES J I)
J))))
(PROVE-LEMMA LESSP-QUOTIENT1 (REWRITE)
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1))))))
(PROVE-LEMMA LESSP-REMAINDER1 (REWRITE)
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y)))))
(DEFN POWER-REP (I BASE)
(IF (ZEROP I)
NIL
(IF (ZEROP BASE)
(CONS I NIL)
(IF (EQUAL BASE 1)
(CONS I NIL)
(CONS (REMAINDER I BASE)
(POWER-REP (QUOTIENT I BASE)
BASE))))))
(PROVE-LEMMA POWER-EVAL-POWER-REP (REWRITE)
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I)))
(PROVE-LEMMA CORRECTNESS-OF-BIG-PLUS (REWRITE)
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
0 BASE)
BASE)
(PLUS I J)))
(DEFN GCD (X Y)
(IF (ZEROP X)
(FIX Y)
(IF (ZEROP Y)
X
(IF (LESSP X Y)
(GCD X (DIFFERENCE Y X))
(GCD (DIFFERENCE X Y)
Y))))
((LEX2 (LIST (COUNT X)
(COUNT Y)))))
(PROVE-LEMMA NUMBERP-GCD (REWRITE)
(NUMBERP (GCD X Y)))
(PROVE-LEMMA GCD-EQUAL-0 (REWRITE)
(EQUAL (EQUAL (GCD X Y)
0)
(AND (ZEROP X)
(ZEROP Y))))
(PROVE-LEMMA GCD-0 (REWRITE)
(EQUAL (GCD 0 Y)
(FIX Y)))
(PROVE-LEMMA COMMUTATIVITY-OF-GCD (REWRITE)
(EQUAL (GCD X Y)
(GCD Y X)))
(PROVE-LEMMA NTH-APPEND (REWRITE)
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A))))))
(PROVE-LEMMA DIFFERENCE-PLUS1 (REWRITE)
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y)))
(PROVE-LEMMA DIFFERENCE-PLUS2 (REWRITE)
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y)))
(PROVE-LEMMA DIFFERENCE-PLUS-CANCELATION (REWRITE)
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z)))
(PROVE-LEMMA TIMES-DIFFERENCE (REWRITE)
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X))))
(DEFN DIVIDES (X Y)
(ZEROP (REMAINDER Y X)))
(PROVE-LEMMA DIVIDES-TIMES (REWRITE)
(EQUAL (REMAINDER (TIMES X Z)
Z)
0))
(PROVE-LEMMA DIFFERENCE-PLUS3 (REWRITE)
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C)))
(PROVE-LEMMA DIFFERENCE-ADD1-CANCELLATION (REWRITE)
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y)))
(PROVE-LEMMA REMAINDER-ADD1 (REWRITE)
(IMPLIES
(AND (NOT (ZEROP Y))
(NOT (EQUAL Y 1)))
(NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y))
Y)
0))))
(PROVE-LEMMA DIVIDES-PLUS-REWRITE1 (REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X Z)
0)
(EQUAL (REMAINDER Y Z)
0))
(EQUAL (REMAINDER (PLUS X Y)
Z)
0)))
(PROVE-LEMMA DIVIDES-PLUS-REWRITE2 (REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X Z)
0)
(NOT (EQUAL (REMAINDER Y Z)
0)))
(NOT (EQUAL (REMAINDER (PLUS X Y)
Z)
0))))
(PROVE-LEMMA DIVIDES-PLUS-REWRITE (REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (PLUS X Y)
Z)
0)
(EQUAL (REMAINDER Y Z)
0))))
(PROVE-LEMMA LESSP-PLUS-CANCELATION (REWRITE)
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z)))
(PROVE-LEMMA DIVIDES-PLUS-REWRITE-COMMUTED (REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (PLUS Y X)
Z)
0)
(EQUAL (REMAINDER Y Z)
0))))
(PROVE-LEMMA EUCLID (REWRITE)
(IMPLIES
(EQUAL (REMAINDER X Z)
0)
(EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X)
Z)
0)
(IF (LESSP X Y)
(EQUAL (REMAINDER Y Z)
0)
T))))
(PROVE-LEMMA LESSP-TIMES-CANCELLATION (REWRITE)
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y))))
(PROVE-LEMMA LESSP-PLUS-CANCELLATION3 (REWRITE)
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X))))
(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-GCD (REWRITE)
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y))))
(PROVE-LEMMA GCD-DIVIDES-BOTH (REWRITE)
(AND (EQUAL (REMAINDER X (GCD X Y))
0)
(EQUAL (REMAINDER Y (GCD X Y))
0)))
(PROVE-LEMMA GCD-IS-THE-GREATEST NIL
(IMPLIES (AND (NOT (ZEROP X))
(NOT (ZEROP Y))
(DIVIDES Z X)
(DIVIDES Z Y))
(LEQ Z (GCD X Y))))
(ADD-SHELL CONS-IF NIL IF-EXPRP ((TEST (NONE-OF)
ZERO)
(LEFT-BRANCH (NONE-OF)
ZERO)
(RIGHT-BRANCH (NONE-OF)
ZERO)))
(DEFN ASSIGNMENT (VAR ALIST)
(IF (EQUAL VAR T)
T
(IF (EQUAL VAR F)
F
(IF (NLISTP ALIST)
F
(IF (EQUAL VAR (CAAR ALIST))
(CDAR ALIST)
(ASSIGNMENT VAR (CDR ALIST)))))))
(DEFN VALUE (X ALIST)
(IF (IF-EXPRP X)
(IF (VALUE (TEST X)
ALIST)
(VALUE (LEFT-BRANCH X)
ALIST)
(VALUE (RIGHT-BRANCH X)
ALIST))
(ASSIGNMENT X ALIST)))
(DEFN IF-DEPTH (X)
(IF (IF-EXPRP X)
(ADD1 (IF-DEPTH (TEST X)))
0))
(DEFN IF-COMPLEXITY (X)
(IF (IF-EXPRP X)
(TIMES (IF-COMPLEXITY (TEST X))
(PLUS (IF-COMPLEXITY (LEFT-BRANCH X))
(IF-COMPLEXITY (RIGHT-BRANCH X))))
1))
(PROVE-LEMMA IF-COMPLEXITY-NOT-0 (REWRITE)
(NOT (EQUAL (IF-COMPLEXITY X)
0)))
(PROVE-LEMMA IF-COMPLEXITY-GOES-DOWN1 (REWRITE)
(IMPLIES (IF-EXPRP X)
(LESSP (IF-COMPLEXITY (LEFT-BRANCH X))
(IF-COMPLEXITY X))))
(PROVE-LEMMA IF-COMPLEXITY-GOES-DOWN2 (REWRITE)
(IMPLIES (IF-EXPRP X)
(LESSP (IF-COMPLEXITY
(RIGHT-BRANCH X))
(IF-COMPLEXITY X))))
(DEFN NORMALIZE
(X)
(IF (IF-EXPRP X)
(IF (IF-EXPRP (TEST X))
(NORMALIZE (CONS-IF (TEST (TEST X))
(CONS-IF
(LEFT-BRANCH (TEST X))
(LEFT-BRANCH X)
(RIGHT-BRANCH X))
(CONS-IF
(RIGHT-BRANCH (TEST X))
(LEFT-BRANCH X)
(RIGHT-BRANCH X))))
(CONS-IF (TEST X)
(NORMALIZE (LEFT-BRANCH X))
(NORMALIZE (RIGHT-BRANCH X))))
X)
((LEX2 (LIST (IF-COMPLEXITY X)
(IF-DEPTH X)))))
(DEFN NORMALIZED-IF-EXPRP (X)
(IF (IF-EXPRP X)
(AND (NOT (IF-EXPRP (TEST X)))
(NORMALIZED-IF-EXPRP (LEFT-BRANCH X))
(NORMALIZED-IF-EXPRP (RIGHT-BRANCH X)))
T))
(DEFN ASSIGNEDP (VAR ALIST)
(IF (EQUAL VAR T)
T
(IF (EQUAL VAR F)
T
(IF (NLISTP ALIST)
F
(IF (EQUAL VAR (CAAR ALIST))
T
(ASSIGNEDP VAR (CDR ALIST)))))))
(DEFN ASSUME-TRUE (VAR ALIST)
(CONS (CONS VAR T)
ALIST))
(DEFN ASSUME-FALSE (VAR ALIST)
(CONS (CONS VAR F)
ALIST))
(DEFN TAUTOLOGYP (X ALIST)
(IF (IF-EXPRP X)
(IF (ASSIGNEDP (TEST X)
ALIST)
(IF (ASSIGNMENT (TEST X)
ALIST)
(TAUTOLOGYP (LEFT-BRANCH X)
ALIST)
(TAUTOLOGYP (RIGHT-BRANCH X)
ALIST))
(AND (TAUTOLOGYP (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(TAUTOLOGYP (RIGHT-BRANCH X)
(ASSUME-FALSE (TEST X)
ALIST))))
(ASSIGNMENT X ALIST)))
(PROVE-LEMMA ASSIGNMENT-APPEND (REWRITE)
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B))))
(PROVE-LEMMA VALUE-CAN-IGNORE-REDUNDANT-ASSIGNMENTS (REWRITE)
(AND (IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
(VALUE X A))
(VALUE X (CONS (CONS VAR VAL)
A)))
(IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
(NOT (VALUE X A)))
(NOT (VALUE X (CONS (CONS VAR VAL)
A))))))
(PROVE-LEMMA VALUE-SHORT-CUT (REWRITE)
(IMPLIES (AND (IF-EXPRP X)
(NORMALIZED-IF-EXPRP X))
(EQUAL (VALUE (TEST X)
A)
(ASSIGNMENT (TEST X)
A))))
(PROVE-LEMMA ASSIGNMENT-IMPLIES-ASSIGNED (REWRITE)
(IMPLIES (ASSIGNMENT X A)
(ASSIGNEDP X A)))
(PROVE-LEMMA TAUTOLOGYP-IS-SOUND (REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(TAUTOLOGYP X A1))
(VALUE X (APPEND A1 A2))))
(DEFN TAUTOLOGY-CHECKER (X)
(TAUTOLOGYP (NORMALIZE X)
NIL))
(DEFN FALSIFY1 (X ALIST)
(IF (IF-EXPRP X)
(IF (ASSIGNEDP (TEST X)
ALIST)
(IF (ASSIGNMENT (TEST X)
ALIST)
(FALSIFY1 (LEFT-BRANCH X)
ALIST)
(FALSIFY1 (RIGHT-BRANCH X)
ALIST))
(IF (FALSIFY1 (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(FALSIFY1 (LEFT-BRANCH X)
(ASSUME-TRUE (TEST X)
ALIST))
(FALSIFY1 (RIGHT-BRANCH X)
(ASSUME-FALSE (TEST X)
ALIST))))
(IF (ASSIGNEDP X ALIST)
(IF (ASSIGNMENT X ALIST)
F ALIST)
(CONS (CONS X F)
ALIST))))
(DEFN FALSIFY (X)
(FALSIFY1 (NORMALIZE X)
NIL))
(PROVE-LEMMA FALSIFY1-EXTENDS-MODELS (REWRITE)
(IMPLIES (ASSIGNEDP X A)
(EQUAL (ASSIGNMENT X (FALSIFY1 Y A))
(IF (FALSIFY1 Y A)
(ASSIGNMENT X A)
(EQUAL X T)))))
(PROVE-LEMMA FALSIFY1-FALSIFIES (REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(FALSIFY1 X A))
(EQUAL (VALUE X (FALSIFY1 X A))
F)))
(PROVE-LEMMA TAUTOLOGYP-FAILS-MEANS-FALSIFY1-WINS (REWRITE)
(IMPLIES (AND (NORMALIZED-IF-EXPRP X)
(NOT (TAUTOLOGYP X A))
A)
(FALSIFY1 X A)))
(PROVE-LEMMA NORMALIZE-IS-SOUND (REWRITE)
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A)))
(PROVE-LEMMA NORMALIZE-NORMALIZES (REWRITE)
(NORMALIZED-IF-EXPRP (NORMALIZE X)))
(PROVE-LEMMA TAUTOLOGY-CHECKER-COMPLETENESS-BRIDGE (REWRITE)
(IMPLIES (AND (EQUAL (VALUE Y (FALSIFY1 X A))
(VALUE X (FALSIFY1 X A)))
(FALSIFY1 X A)
(NORMALIZED-IF-EXPRP X))
(EQUAL (VALUE Y (FALSIFY1 X A))
F)))
(PROVE-LEMMA TAUTOLOGY-CHECKER-IS-COMPLETE NIL
(IMPLIES (NOT (TAUTOLOGY-CHECKER X))
(EQUAL (VALUE X (FALSIFY X))
F)))
(PROVE-LEMMA TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE (REWRITE)
(IMPLIES (AND (TAUTOLOGYP Y A1)
(NORMALIZED-IF-EXPRP Y)
(EQUAL (VALUE X A2)
(VALUE Y (APPEND A1 A2))))
(VALUE X A2)))
(PROVE-LEMMA TAUTOLOGY-CHECKER-IS-SOUND NIL
(IMPLIES (TAUTOLOGY-CHECKER X)
(VALUE X A)))
;; (SWAP-OUT "P-TEMP")
(MAKE-LIB "P-TEMP")
(NOTE-LIB "P-TEMP.LIB" "P-TEMP.LISP")
(PROVE-LEMMA FLATTEN-SINGLETON (REWRITE)
(EQUAL (EQUAL (FLATTEN X)
(CONS Y NIL))
(AND (NLISTP X)
(EQUAL X Y))))
(DEFN LEFTCOUNT (X)
(IF (NLISTP X)
0
(ADD1 (LEFTCOUNT (CAR X)))))
(DEFN GOPHER (X)
(IF (OR (NLISTP X)
(NLISTP (CAR X)))
X
(GOPHER (CONS (CAAR X)
(CONS (CDAR X)
(CDR X)))))
((LESSP (LEFTCOUNT X))))
(PROVE-LEMMA GOPHER-PRESERVES-COUNT (REWRITE)
(NOT (LESSP (COUNT X)
(COUNT (GOPHER X)))))
(PROVE-LEMMA LISTP-GOPHER (REWRITE)
(EQUAL (LISTP (GOPHER X))
(LISTP X)))
(DEFN SAMEFRINGE (X Y)
(IF (OR (NLISTP X)
(NLISTP Y))
(EQUAL X Y)
(AND (EQUAL (CAR (GOPHER X))
(CAR (GOPHER Y)))
(SAMEFRINGE (CDR (GOPHER X))
(CDR (GOPHER Y))))))
(PROVE-LEMMA GOPHER-RETURNS-LEFTMOST-ATOM (REWRITE)
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
0)))
(PROVE-LEMMA GOPHER-RETURNS-CORRECT-STATE (REWRITE)
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS 0 NIL))))
(PROVE-LEMMA CORRECTNESS-OF-SAMEFRINGE (REWRITE)
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y))))
(DEFN PRIME1 (X Y)
(IF (ZEROP Y)
F
(IF (EQUAL Y 1)
T
(AND (NOT (DIVIDES Y X))
(PRIME1 X (SUB1 Y))))))
(DEFN PRIME (X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X 1))
(PRIME1 X (SUB1 X))))
(DEFN GREATEST-FACTOR (X Y)
(IF (OR (ZEROP Y)
(EQUAL Y 1))
X
(IF (DIVIDES Y X)
Y
(GREATEST-FACTOR X (SUB1 Y)))))
(PROVE-LEMMA GREATEST-FACTOR-LESSP (REWRITE)
(IMPLIES (AND (LESSP Y X)
(NOT (PRIME1 X Y))
(NOT (ZEROP X))
(NOT (EQUAL (SUB1 X)
0))
(NOT (ZEROP Y)))
(LESSP (GREATEST-FACTOR X Y)
X)))
(PROVE-LEMMA GREATEST-FACTOR-DIVIDES (REWRITE)
(IMPLIES (AND (LESSP Y X)
(NOT (PRIME1 X Y))
(NOT (ZEROP X))
(NOT (EQUAL X 1))
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X
(GREATEST-FACTOR X Y))
0)))
(PROVE-LEMMA GREATEST-FACTOR-0 (REWRITE)
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
0)
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X 0))))
(PROVE-LEMMA REMAINDER-0-CROCK (REWRITE)
(EQUAL (REMAINDER 0 Y)
0)
NIL
; We have to prove this to get (REMAINDER 1 Y) to open in GREATEST-FACTOR-1.
; If CURRENT-CL moved we wouldn't have to do it.
)
(PROVE-LEMMA GREATEST-FACTOR-1 (REWRITE)
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1)))
(PROVE-LEMMA NUMBERP-GREATEST-FACTOR (REWRITE)
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X))))))
(DEFN
PRIME-FACTORS
(X)
(IF (OR (ZEROP X)
(EQUAL (SUB1 X)
0))
NIL
(IF (PRIME1 X (SUB1 X))
(CONS X NIL)
(APPEND (PRIME-FACTORS (GREATEST-FACTOR X
(SUB1 X)))
(PRIME-FACTORS
(QUOTIENT X (GREATEST-FACTOR X (SUB1 X))))))))
(DEFN PRIME-LIST (L)
(IF (NLISTP L)
T
(AND (PRIME (CAR L))
(PRIME-LIST (CDR L)))))
(DEFN TIMES-LIST (L)
(IF (NLISTP L)
1
(TIMES (CAR L)
(TIMES-LIST (CDR L)))))
(PROVE-LEMMA TIMES-LIST-APPEND (REWRITE)
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y))))
(PROVE-LEMMA PRIME-LIST-APPEND (REWRITE)
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y))))
(PROVE-LEMMA PRIME-LIST-PRIME-FACTORS (REWRITE)
(PRIME-LIST (PRIME-FACTORS X)))
(PROVE-LEMMA QUOTIENT-TIMES1 (REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NUMBERP X)
(NOT (EQUAL X 0))
(DIVIDES X Y))
(EQUAL (TIMES X (QUOTIENT Y X))
Y)))
(PROVE-LEMMA QUOTIENT-LESSP (REWRITE)
(IMPLIES (AND (NOT (ZEROP X))
(LESSP X Y))
(NOT (EQUAL (QUOTIENT Y X)
0))))
(PROVE-LEMMA ENOUGH-FACTORS (REWRITE)
(IMPLIES (NOT (ZEROP X))
(EQUAL (TIMES-LIST (PRIME-FACTORS X))
X)))
(PROVE-LEMMA PRIME-FACTORIZATION-EXISTENCE NIL
(IMPLIES
(NOT (ZEROP X))
(AND (EQUAL (TIMES-LIST (PRIME-FACTORS X))
X)
(PRIME-LIST (PRIME-FACTORS X)))))
(DEFN GREATEREQPR (W Z)
(IF (ZEROP W)
(ZEROP Z)
(IF (EQUAL W Z)
T
(GREATEREQPR (SUB1 W)
Z))))
(PROVE-LEMMA TIMES-ID-IFF-1 (REWRITE)
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z 0)
(EQUAL W 1)))))
(PROVE-LEMMA PRIME1-BASIC (REWRITE)
(IMPLIES (AND (NOT (EQUAL Z 1))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(GREATEREQPR U Z))
(NOT (PRIME1 (TIMES W Z)
U))))
(PROVE-LEMMA GREATEREQPR-LESSP (REWRITE)
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y))))
(PROVE-LEMMA GREATEREQPR-REMAINDER (REWRITE)
(IMPLIES (AND (NOT (EQUAL Z (ADD1 V)))
(DIVIDES Z (ADD1 V)))
(GREATEREQPR V Z)))
(PROVE-LEMMA PRIME-BASIC (REWRITE)
(IMPLIES (AND (NOT (EQUAL Z 1))
(NOT (EQUAL Z X))
(NOT (ZEROP X))
(NOT (EQUAL X 1))
(DIVIDES Z X))
(NOT (PRIME1 X (SUB1 X)))))
(PROVE-LEMMA REMAINDER-GCD (REWRITE)
(IMPLIES (EQUAL (GCD B X)
Y)
(EQUAL (REMAINDER B Y)
0)))
(PROVE-LEMMA REMAINDER-GCD-1 (REWRITE)
(IMPLIES (NOT (EQUAL (REMAINDER B X)
0))
(NOT (EQUAL (GCD B X)
X))))
(PROVE-LEMMA DIVIDES-TIMES1 (REWRITE)
(IMPLIES (EQUAL A (TIMES Z Y))
(EQUAL (REMAINDER A Z)
0)))
(PROVE-LEMMA TIMES-IDENTITY1 (REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 1))
(NOT (EQUAL Y 0))
(NOT (EQUAL X 0)))
(NOT (EQUAL X (TIMES X Y)))))
(PROVE-LEMMA TIMES-IDENTITY (REWRITE)
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X 0)
(AND (NUMBERP X)
(EQUAL Y 1)))))
(PROVE-LEMMA KLUDGE-BRIDGE (REWRITE)
(IMPLIES (EQUAL Y (TIMES K X))
(EQUAL (GCD Y (TIMES A X))
(TIMES X (GCD A K)))))
(PROVE-LEMMA HACK1 (REWRITE)
(IMPLIES (AND (NOT (DIVIDES X A))
(EQUAL A (GCD (TIMES X A)
(TIMES B A))))
(NOT (EQUAL (TIMES K X)
(TIMES B A)))))
(PROVE-LEMMA PRIME-GCD (REWRITE)
(IMPLIES (AND (NOT (DIVIDES X B))
(NOT (ZEROP X))
(NOT (EQUAL (SUB1 X)
0))
(PRIME1 X (SUB1 X)))
(EQUAL (EQUAL (GCD B X)
1)
T))
NIL
; The third hyp is that X is not 1; we have phrased it oddly on purpose. The
; more natural phrasing causes us to fail to prove this theorem. The problem
; is that the proof requires an appeal to PRIME-BASIC in which the free var Z
; is instantiated to be (GCD B X) -- which is guessed by instantiating the
; hyp (NOT (EQUAL Z 1)) and that instantiation is screwed if we put among our
; hyps (NOT (EQUAL X 1)).
)
(PROVE-LEMMA GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES (REWRITE)
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL FREE (TIMES X Z)))
(EQUAL (GCD (TIMES B Z)
FREE)
(TIMES Z (GCD B X))))
NIL
; As is evident from the name, this stupid lemma is necessary because of a
; Knuth-Bendix type problem. Had X*Z not been expanded we could have used the
; more elegant DISTRIBUTIVITY-OF-TIMES-OVER-GCD. This lemma has a further
; twist. X is a free var. to cut down on the frequency with which this lemma
; is tried. Once, (NOT (EQUAL X 0)) was the first hyp. It happened that in
; there were three possibly choices for X from the TYPE-ALIST at run time,
; but that the first one was correct. Unfortunately, when we changed the
; order of evaluation of the lits in a clause, the correct choice was
; obscured. Luckily, by keying on the NUMBERP hyp we can still get the tp to
; chose the right X. The other two choices are both numeric -- they are
; REMAINDER expressions -- but the fact that they are numeric is not stored
; on the TYPE-ALIST, thank goodness! Isn't that dreadful?
)
(PROVE-LEMMA PRIME-KEY (REWRITE)
(IMPLIES (AND (NUMBERP Z)
(PRIME X)
(NOT (DIVIDES X Z))
(NOT (DIVIDES X B)))
(NOT (EQUAL (TIMES X K)
(TIMES B Z)))))
(PROVE-LEMMA
QUOTIENT-DIVIDES
(REWRITE)
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL (TIMES X (QUOTIENT Y X))
Y)))
(NOT (EQUAL (REMAINDER Y X)
0))))
(PROVE-LEMMA LITTLE-STEP (REWRITE)
(IMPLIES (AND (PRIME X)
(NOT (EQUAL Y 1))
(NOT (EQUAL X Y)))
(NOT (EQUAL (REMAINDER X Y)
0))))
(PROVE-LEMMA LESSP-COUNT-DELETE (REWRITE)
(IMPLIES (MEMBER N L)
(LESSP (COUNT (DELETE N L))
(COUNT L))))
(DEFN PERM (A B)
(IF (NLISTP A)
(NLISTP B)
(IF (MEMBER (CAR A)
B)
(PERM (CDR A)
(DELETE (CAR A)
B))
F)))
(PROVE-LEMMA REMAINDER-TIMES (REWRITE)
(EQUAL (REMAINDER (TIMES Y X)
Y)
0))
(PROVE-LEMMA PRIME-LIST-DELETE (REWRITE)
(IMPLIES (PRIME-LIST L2)
(PRIME-LIST (DELETE X L2))))
(PROVE-LEMMA DIVIDES-TIMES-LIST (REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(MEMBER C L))
(EQUAL (REMAINDER (TIMES-LIST L)
C)
0)))
(PROVE-LEMMA QUOTIENT-TIMES (REWRITE)
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
0
(FIX X))))
(PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES (REWRITE)
(IMPLIES (AND (NOT (ZEROP A))
(DIVIDES A W))
(EQUAL (TIMES C (QUOTIENT W A))
(QUOTIENT (TIMES C W)
A))))
(PROVE-LEMMA TIMES-LIST-DELETE (REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(MEMBER C L))
(EQUAL (TIMES-LIST (DELETE C L))
(QUOTIENT (TIMES-LIST L)
C))))
(PROVE-LEMMA PRIME-LIST-TIMES-LIST (REWRITE)
(IMPLIES
(AND (PRIME C)
(PRIME-LIST L2)
(NOT (MEMBER C L2)))
(NOT (EQUAL (REMAINDER (TIMES-LIST L2)
C)
0))))
(PROVE-LEMMA IF-TIMES-THEN-DIVIDES (REWRITE)
(IMPLIES (AND (NOT (ZEROP C))
(NOT (DIVIDES C X)))
(NOT (EQUAL (TIMES C Y)
X))))
(PROVE-LEMMA TIMES-EQUAL-1 (REWRITE)
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A 0))
(NOT (EQUAL B 0))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
0)
(EQUAL (SUB1 B)
0))))
(PROVE-LEMMA PRIME-MEMBER (REWRITE)
(IMPLIES (AND (EQUAL (TIMES C (TIMES-LIST L1))
(TIMES-LIST L2))
(PRIME C)
(PRIME-LIST L2))
(MEMBER C L2))
((DISABLE TIMES)))
(PROVE-LEMMA DIVIDES-IMPLIES-TIMES (REWRITE)
(IMPLIES (AND (NOT (ZEROP A))
(NUMBERP C)
(EQUAL (TIMES A C)
B))
(EQUAL (EQUAL C (QUOTIENT B A))
T)))
(PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS NIL
(IMPLIES (AND (PRIME-LIST L1)
(PRIME-LIST L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2)))
(PERM L1 L2)))
(DEFN MAXIMUM (L)
(IF (NLISTP L)
0
(IF (LESSP (CAR L)
(MAXIMUM (CDR L)))
(MAXIMUM (CDR L))
(CAR L))))
(PROVE-LEMMA MEMBER-MAXIMUM (REWRITE)
(IMPLIES (LISTP X)
(MEMBER (MAXIMUM X)
X)))
(PROVE-LEMMA LESSP-DELETE-REWRITE (REWRITE)
(EQUAL (LESSP (COUNT (DELETE X L))
(COUNT L))
(MEMBER X L)))
(DEFN ORDERED2 (L)
(IF (LISTP L)
(IF (LISTP (CDR L))
(IF (LESSP (CAR L)
(CADR L))
F
(ORDERED2 (CDR L)))
T)
T))
(DEFN DSORT (L)
(IF (NLISTP L)
NIL
(CONS (MAXIMUM L)
(DSORT (DELETE (MAXIMUM L)
L)))))
(DEFN ADDTOLIST2 (X L)
(IF (LISTP L)
(IF (LESSP X (CAR L))
(CONS (CAR L)
(ADDTOLIST2 X (CDR L)))
(CONS X L))
(CONS X NIL)))
(DEFN SORT2 (L)
(IF (NLISTP L)
NIL
(ADDTOLIST2 (CAR L)
(SORT2 (CDR L)))))
(PROVE-LEMMA SORT2-GEN-1 (REWRITE)
(PLISTP (SORT2 X)))
(PROVE-LEMMA SORT2-GEN-2 (REWRITE)
(ORDERED2 (SORT2 X)))
(PROVE-LEMMA SORT2-GEN (GENERALIZE)
(AND (PLISTP (SORT2 X))
(ORDERED2 (SORT2 X))))
(PROVE-LEMMA ADDTOLIST2-DELETE (REWRITE)
(IMPLIES (AND (PLISTP Y)
(ORDERED2 Y)
(NOT (EQUAL X V)))
(EQUAL (ADDTOLIST2 V (DELETE X Y))
(DELETE X (ADDTOLIST2 V Y)))))
(PROVE-LEMMA DELETE-ADDTOLIST2 (REWRITE)
(IMPLIES (PLISTP Y)
(EQUAL (DELETE V (ADDTOLIST2 V Y))
Y)))
(PROVE-LEMMA ADDTOLIST2-KLUDGE (REWRITE)
(IMPLIES (AND (NOT (LESSP V W))
(EQUAL (ADDTOLIST2 V Y)
(CONS V Y)))
(EQUAL (ADDTOLIST2 V (ADDTOLIST2 W Y))
(CONS V (ADDTOLIST2 W Y)))))
(PROVE-LEMMA LESSP-MAXIMUM-ADDTOLIST2 (REWRITE)
(IMPLIES (NOT (LESSP V (MAXIMUM Z)))
(EQUAL (ADDTOLIST2 V (SORT2 Z))
(CONS V (SORT2 Z)))))
(PROVE-LEMMA SORT2-DELETE-CONS (REWRITE)
(IMPLIES (LISTP X)
(EQUAL (CONS (MAXIMUM X)
(DELETE (MAXIMUM X)
(SORT2 X)))
(SORT2 X))))
(PROVE-LEMMA SORT2-DELETE (REWRITE)
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L))))
(PROVE-LEMMA DSORT-SORT2 (REWRITE)
(EQUAL (DSORT X)
(SORT2 X)))
(PROVE-LEMMA COUNT-LIST-SORT2 NIL
(EQUAL (COUNT-LIST A (SORT2 L))
(COUNT-LIST A L)))
; The next segment of this XXX illustrates three different program
; verification methods: the functional approach, the inductive assertion
; approach, and the interpreter approach. The program considered is a simple
; loop for summing the numbers from I down to 0
(DEFN SIGMA (M N)
(IF (LESSP M N)
(PLUS N (SIGMA M (SUB1 N)))
0)
NIL
; With each program verification method we will prove that the program
; computes (SIGMA 0 I); at the end of this exercise we prove that (SIGMA 0 I)
; is I*I+1/2.
)
(PROVE-LEMMA DIFFERENCE-1 (REWRITE)
(EQUAL (DIFFERENCE X 1)
(SUB1 X)))
(DEFN PROG-TRANS-OF-SIGMA (I AC)
(IF (ZEROP I)
AC
(PROG-TRANS-OF-SIGMA (DIFFERENCE I 1)
(PLUS AC I))))
(PROVE-LEMMA FUNCTIONAL-LOOP-INVRT (REWRITE)
(IMPLIES (NUMBERP AC)
(EQUAL (PROG-TRANS-OF-SIGMA I AC)
(PLUS AC (SIGMA 0 I)))))
(PROVE-LEMMA CORRECTNESS-OF-FUNCTIONAL-SIGMA NIL
(EQUAL (PROG-TRANS-OF-SIGMA I 0)
(SIGMA 0 I)))
(PROVE-LEMMA SIGMA-INPUT-PATH NIL (AND (EQUAL 0 (SIGMA K K))
(LEQ K K)))
(PROVE-LEMMA SIGMA-LOOP-INVRT NIL
(IMPLIES (AND (NOT (ZEROP I))
(LEQ I K))
(AND (EQUAL (PLUS (SIGMA I K)
I)
(SIGMA (SUB1 I)
K))
(LEQ (SUB1 I)
K))))
(PROVE-LEMMA SIGMA-OUTPUT-PATH NIL
(IMPLIES (AND (ZEROP I)
(LEQ I K))
(EQUAL (SIGMA I K)
(SIGMA 0 K))))
; The interpreter we consider fetches instructions out of the same memory
; being modified by the execution. Earlier we proved a simpler version in
; which the program was in read-only memory. The new approach is almost
; identical but we have to force the opening up of certain functions because
; instead of doing CDR recursion the interpreter EXECUTE1 has to count the PC
; up and the theorem prover doesn't handle counting up very well yet.
(DEFN SET (ADDR VAL MEM)
(IF (ZEROP ADDR)
(CONS VAL (CDR MEM))
(CONS (CAR MEM)
(SET (SUB1 ADDR)
VAL
(CDR MEM)))))
(DEFN GET (ADDR MEM)
(IF (ZEROP ADDR)
(CAR MEM)
(GET (SUB1 ADDR)
(CDR MEM))))
(PROVE-LEMMA GET-SET (REWRITE)
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM))))
(DEFN
EXECUTE1
(PC MEM MAX)
(IF
(NOT (LESSP PC MAX))
(LIST F MEM)
(IF
(EQUAL (GET PC MEM)
(QUOTE (STOP)))
(LIST F MEM)
(IF
(EQUAL (CAR (GET PC MEM))
(QUOTE JUMPA))
(LIST (CADR (GET PC MEM))
MEM)
(IF
(EQUAL (CAR (GET PC MEM))
(QUOTE SKIPNE))
(IF (ZEROP (GET (CADR (GET PC MEM))
MEM))
(EXECUTE1 (ADD1 PC)
MEM MAX)
(EXECUTE1 (ADD1 (ADD1 PC))
MEM MAX))
(IF
(EQUAL (CAR (GET PC MEM))
(QUOTE SUBI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(DIFFERENCE (GET (CADR (GET PC MEM))
MEM)
(CADDR (GET PC MEM)))
MEM)
MAX)
(IF
(EQUAL (CAR (GET PC MEM))
(QUOTE ADDI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(PLUS (CADDR (GET PC MEM))
(GET (CADR (GET PC MEM))
MEM))
MEM)
MAX)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE ADD))
(EXECUTE1
(ADD1 PC)
(SET (CADR (GET PC MEM))
(PLUS (GET (CADDR (GET PC MEM))
MEM)
(GET (CADR (GET PC MEM))
MEM))
MEM)
MAX)
(IF (EQUAL (CAR (GET PC MEM))
(QUOTE MOVEI))
(EXECUTE1 (ADD1 PC)
(SET (CADR (GET PC MEM))
(CADDR (GET PC MEM))
MEM)
MAX)
(LIST F MEM)))))))))
((LESSP (DIFFERENCE MAX PC))))
(DEFN EXECUTE (PC MEM CLK)
(IF (ZEROP CLK)
MEM
(IF (NUMBERP PC)
(EXECUTE (CAR (EXECUTE1 PC MEM (LENGTH MEM)))
(CADR (EXECUTE1 PC MEM (LENGTH MEM)))
(SUB1 CLK))
MEM)))
(DEFN GET-SIMPLIFIER (X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE GET))
(LISTP (CADR X))
(EQUAL (CAR (CADR X))
(QUOTE QUOTE)))
(IF (ZEROP (CADR (CADR X)))
(LIST (QUOTE CAR)
(CADDR X))
(LIST (QUOTE GET)
(LIST (QUOTE QUOTE)
(SUB1 (CADR (CADR X))))
(LIST (QUOTE CDR)
(CADDR X))))
X))
(PROVE-LEMMA CORRECTNESS-OF-GET-SIMPLIFIER ((META GET))
(IMPLIES
(FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (GET-SIMPLIFIER X)
A))
(FORMP (GET-SIMPLIFIER X)))))
(DEFN
SET-SIMPLIFIER
(X)
(IF (AND (LISTP X)
(EQUAL (CAR X)
(QUOTE SET))
(LISTP (CADR X))
(EQUAL (CAR (CADR X))
(QUOTE QUOTE)))
(IF (ZEROP (CADR (CADR X)))
(LIST (QUOTE CONS)
(CADDR X)
(LIST (QUOTE CDR)
(CADDDR X)))
(LIST (QUOTE CONS)
(LIST (QUOTE CAR)
(CADDDR X))
(LIST (QUOTE SET)
(LIST (QUOTE QUOTE)
(SUB1 (CADR (CADR X))))
(CADDR X)
(LIST (QUOTE CDR)
(CADDDR X)))))
X))
(PROVE-LEMMA CORRECTNESS-OF-SET-SIMPLIFIER ((META SET))
(IMPLIES
(FORMP X)
(AND (EQUAL (MEANING X A)
(MEANING (SET-SIMPLIFIER X)
A))
(FORMP (SET-SIMPLIFIER X)))))
(PROVE-LEMMA LENGTH-5 (REWRITE)
(IMPLIES (EQUAL (CADDDDR X)
(QUOTE (JUMPA 1)))
(EQUAL (LENGTH X)
(PLUS 5 (LENGTH (CDDDDDR X)))))
NIL
; To relieve the hyp that MAX is greater than 6 in EXECUTE1-OPENED-UP, we
; need to know that (LENGTH MEM) there is greater than six. We have an
; explicit picture of the first 6 elements of MEM, so it suffices just to
; expand (LENGTH MEM) into 6 + (LENGTH ...). This rather clear picture of
; things is messed up slightly because the tp expands LENGTH once on its own.
; So this lemma forces the other five.
)
(PROVE-LEMMA
LENGTH-CONS6
(REWRITE)
(EQUAL (LENGTH (CONS X1
(CONS X2 (CONS X3
(CONS X4
(CONS X5
(CONS X6 X7)))
))))
(PLUS 6 (LENGTH X7))))
(PROVE-LEMMA
EXECUTE1-1
(REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL
(EXECUTE1
1
(CONS
(QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(IF
(ZEROP (CAR L))
(EXECUTE1
2
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1
3
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX))))
NIL
; This and the next few lemmas are required to force EXECUTE1 to open up when
; given explicit PCs. Without these lemmas the stupid theorem prover refused
; to expand (EXECUTE1 3 --) to (EXECUTE 4 --) because it doesn't think
; anything has improved since MEM is more complicated.
)
(PROVE-LEMMA
EXECUTE1-3
(REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL
(EXECUTE1
3
(CONS
(QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1
4
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS
(QUOTE (STOP))
(CONS
(QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (CAR L)
(CONS (PLUS (CAR L)
(CADR L))
(CDDR L)))))))))
MAX))))
(PROVE-LEMMA
EXECUTE1-4
(REWRITE)
(IMPLIES
(NOT (LESSP MAX 6))
(EQUAL
(EXECUTE1
4
(CONS
(QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
L))))))
MAX)
(EXECUTE1
5
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS
(QUOTE (STOP))
(CONS
(QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (DIFFERENCE (CAR L)
1)
(CDR L))))))))
MAX))))
(PROVE-LEMMA
EXECUTE1-OPENED-UP
(REWRITE)
(IMPLIES
(AND (NOT (LESSP MAX 6))
(EQUAL (CAR MEM)
(QUOTE (MOVEI 7 0)))
(EQUAL (CADR MEM)
(QUOTE (SKIPNE 6)))
(EQUAL (CADDR MEM)
(QUOTE (STOP)))
(EQUAL (CADDDR MEM)
(QUOTE (ADD 7 6)))
(EQUAL (CADDDDR MEM)
(QUOTE (SUBI 6 1)))
(EQUAL (CADDDDDR MEM)
(QUOTE (JUMPA 1))))
(EQUAL
(EXECUTE1 1 MEM MAX)
(IF
(ZEROP (CADDDDDDR MEM))
(LIST
F
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CDDDDDDR MEM))))))))
(LIST
1
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS
(QUOTE (STOP))
(CONS
(QUOTE (ADD 7 6))
(CONS
(QUOTE (SUBI 6 1))
(CONS
(QUOTE (JUMPA 1))
(CONS (SUB1 (CADDDDDDR MEM))
(CONS (PLUS (CADDDDDDR MEM)
(CADDDDDDDR MEM))
(CDDDDDDDDR MEM))))))))))))))
(PROVE-LEMMA
EXECUTE-OPENED-UP
(REWRITE)
(IMPLIES (AND (NUMBERP PC)
(NOT (ZEROP CLK)))
(EQUAL (EXECUTE PC MEM CLK)
(EXECUTE (CAR (EXECUTE1 PC MEM (LENGTH MEM)))
(CADR (EXECUTE1 PC MEM
(LENGTH MEM)))
(SUB1 CLK))))
NIL
; This lemma forces EXECUTE to open even though it has calls of EXECUTE1 in
; it that might not occur in the thm. Without this lemma we don't expand
; EXECUTE even when we have (SUB1 CLK) in the problem because of the
; EXECUTE1s. What is so maddening is that after an ELIM on CLK we do expand
; it. But in some of the cases things get messy because some other elims
; happen first. I am not sure if we could prove it without this lemma, but if
; so it takes an awfully long time.
)
(PROVE-LEMMA
INTERPRETER-LOOP-INVRT
(REWRITE)
(IMPLIES (AND (NOT (LESSP CLK (CADDDDDDR MEM)))
(EQUAL (CAR MEM)
(QUOTE (MOVEI 7 0)))
(EQUAL (CADR MEM)
(QUOTE (SKIPNE 6)))
(EQUAL (CADDR MEM)
(QUOTE (STOP)))
(EQUAL (CADDDR MEM)
(QUOTE (ADD 7 6)))
(EQUAL (CADDDDR MEM)
(QUOTE (SUBI 6 1)))
(EQUAL (CADDDDDR MEM)
(QUOTE (JUMPA 1))))
(EQUAL (CADDDDDDDR (EXECUTE 1 MEM CLK))
(IF (ZEROP (CADDDDDDR MEM))
(CADDDDDDDR MEM)
(PLUS (CADDDDDDDR MEM)
(SIGMA 0 (CADDDDDDR MEM))))))
NIL
; Note the careful way I phrased that so that (EXECUTE & MEM CLK) appears so
; we pick MEM up in the induction hyps. Had I phrased the hyps as an equation
; between MEM and a half-constant APPEND the induction wouldn't go through.
)
(PROVE-LEMMA
INTERPRETER-INPUT-PATH
(REWRITE)
(EQUAL
(EXECUTE
0
(CONS
(QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
MEM))))))
CLK)
(IF
(ZEROP CLK)
(CONS
(QUOTE (MOVEI 7 0))
(CONS (QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
MEM))))))
(EXECUTE
1
(CONS
(QUOTE (MOVEI 7 0))
(CONS
(QUOTE (SKIPNE 6))
(CONS (QUOTE (STOP))
(CONS (QUOTE (ADD 7 6))
(CONS (QUOTE (SUBI 6 1))
(CONS (QUOTE (JUMPA 1))
(CONS (CAR MEM)
(CONS 0 (CDDR MEM)))))
))))
CLK)))
NIL
; This one is necessary because we don't open up (EXECUTE 0 & &) so as to hit
; it with the INTERPRETER-LOOP-INVRT unless we have the target in the theorem
; already.
)
(PROVE-LEMMA
CORRECTNESS-OF-INTERPRETED-SIGMA NIL
(IMPLIES (AND (EQUAL MEM (APPEND (QUOTE ((MOVEI 7 0)
(SKIPNE 6)
(STOP)
(ADD 7 6)
(SUBI 6 1)
(JUMPA 1)))
TL))
(EQUAL I (GET 6 MEM))
(NOT (LESSP CLK I)))
(EQUAL (GET 7 (EXECUTE 0 MEM CLK))
(IF (ZEROP CLK)
(GET 7 MEM)
(SIGMA 0 I)))))
(PROVE-LEMMA DIFFERENCE-2 (REWRITE)
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X)))
(PROVE-LEMMA HALF-PLUS (REWRITE)
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2))))
(PROVE-LEMMA SIGMA-IS-HALF-PRODUCT (REWRITE)
(EQUAL (SIGMA 0 I)
(QUOTIENT (TIMES I (ADD1 I))
2)))
(DCL H (X Y))
(ADD-AXIOM H-COMMUTIVITY2 (REWRITE)
(EQUAL (H X (H Y Z))
(H Y (H X Z))))
(DEFN H-PR (L AC)
(IF (NLISTP L)
AC
(H (CAR L)
(H-PR (CDR L)
AC))))
(DEFN H-AC (L AC)
(IF (NLISTP L)
AC
(H-AC (CDR L)
(H (CAR L)
AC))))
(PROVE-LEMMA H-LEMMA (REWRITE)
(EQUAL (H-PR X (H Z A))
(H Z (H-PR X A))))
(PROVE-LEMMA H-EQ (REWRITE)
(EQUAL (H-AC L AC)
(H-PR L AC))
((INDUCT (H-AC L AC))))
(DEFN F0 (X)
(IF (LESSP 100 X)
(DIFFERENCE X 10)
91))
(PROVE-LEMMA F0-SATISFIES-F91-EQUATION NIL
(EQUAL (F0 X)
(IF (LESSP 100 X)
(DIFFERENCE X 10)
(F0 (F0 (PLUS X 11))))))
(REFLECT F91 F0-SATISFIES-F91-EQUATION
((LESSP (DIFFERENCE 101 X))))
(PROVE-LEMMA F91-IS-F0 (REWRITE)
(EQUAL (F91 X)
(F0 X)))
(DEFN EVEN (X)
(EQUAL 0 (REMAINDER X 2)))
(DEFN SQUARE (X)
(TIMES X X))
(PROVE-LEMMA TIMES-1 (REWRITE)
(EQUAL (TIMES 1 X)
(FIX X)))
(PROVE-LEMMA TIMES-2 (REWRITE)
(EQUAL (TIMES 2 X)
(PLUS X X)))
(PROVE-LEMMA EXP-OF-0 (REWRITE)
(EQUAL (EXP 0 K)
(IF (ZEROP K)
1 0)))
(PROVE-LEMMA EXP-OF-1 (REWRITE)
(EQUAL (EXP 1 K)
1))
(PROVE-LEMMA EXP-BY-0 (REWRITE)
(EQUAL (EXP X 0)
1))
(PROVE-LEMMA EXP-TIMES (REWRITE)
(EQUAL (EXP (TIMES I J)
K)
(TIMES (EXP I K)
(EXP J K))))
(PROVE-LEMMA EXP-EXP (REWRITE)
(EQUAL (EXP (EXP I J)
K)
(EXP I (TIMES J K))))
(PROVE-LEMMA REMAINDER-PLUS-TIMES-1 (REWRITE)
(EQUAL (REMAINDER (PLUS X (TIMES I J))
J)
(REMAINDER X J)))
(PROVE-LEMMA REMAINDER-PLUS-TIMES-2 (REWRITE)
(EQUAL (REMAINDER (PLUS X (TIMES J I))
J)
(REMAINDER X J)))
(PROVE-LEMMA REMAINDER-TIMES-1 (REWRITE)
(EQUAL (REMAINDER (TIMES B (TIMES A C))
A)
0))
(PROVE-LEMMA REMAINDER-OF-1 (REWRITE)
(EQUAL (REMAINDER 1 X)
(IF (EQUAL X 1)
0 1)))
(PROVE-LEMMA EQUAL-LENGTH-0 (REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(NLISTP X)))
(PROVE-LEMMA LENGTH-DELETE (REWRITE)
(EQUAL (LENGTH (DELETE X L))
(IF (MEMBER X L)
(LENGTH (CDR L))
(LENGTH L))))
(PROVE-LEMMA REMAINDER-DIFFERENCE-TIMES (REWRITE)
(EQUAL (REMAINDER (DIFFERENCE (TIMES P X)
(TIMES P Y))
P)
0)
((USE (DIVIDES-TIMES (X (DIFFERENCE X Y))
(Z P)))
(DISABLE DIVIDES-TIMES)))
(PROVE-LEMMA PRIME-KEY-REWRITE (REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES A B)
P)
0)
(OR (EQUAL (REMAINDER A P)
0)
(EQUAL (REMAINDER B P)
0))))
((USE (PRIME-KEY (X P)
(B A)
(Z B)
(K (QUOTIENT (TIMES A B)
P)))
(REMAINDER-QUOTIENT (X (TIMES A B))
(Y P)))
(DISABLE PRIME-KEY REMAINDER-QUOTIENT)))
(PROVE-LEMMA TIMES-TIMES-LIST-DELETE (REWRITE)
(IMPLIES (MEMBER X L)
(EQUAL (TIMES X
(TIMES-LIST (DELETE X L)))
(TIMES-LIST L))))
(PROVE-LEMMA LESSP-REMAINDER-DIVISOR (REWRITE)
(IMPLIES (NOT (ZEROP Y))
(LESSP (REMAINDER X Y)
Y)))
(DCL APPLY2 (FN X Y))
(DEFN EVAL2 (FORM ENVRN)
(IF (NUMBERP FORM)
FORM
(IF (LITATOM FORM)
(CDR (ASSOC FORM ENVRN))
(IF (LISTP FORM)
(APPLY2 (CAR FORM)
(EVAL2 (CADR FORM)
ENVRN)
(EVAL2 (CADDR FORM)
ENVRN))
FORM))))
(DEFN SUBST2 (NEW OLD TERM)
(IF (NUMBERP TERM)
TERM
(IF (LITATOM TERM)
(IF (EQUAL OLD TERM)
NEW TERM)
(IF (LISTP TERM)
(LIST (CAR TERM)
(SUBST2 NEW OLD (CADR TERM))
(SUBST2 NEW OLD (CADDR TERM)))
TERM))))
(PROVE-LEMMA SUBST2-OK NIL
(EQUAL (EVAL2 (SUBST2 NEW OLD TERM)
A)
(EVAL2 TERM (CONS (CONS OLD (EVAL2 NEW A))
A)))
NIL))
NIL "PROVEALL")
;;; "RSA"
(PROVEALL
'((NOTE-LIB "PROVEALL.LIB" "PROVEALL.LISP")
(DISABLE EUCLID)
(DISABLE QUOTIENT-DIVIDES)
(DISABLE IF-TIMES-THEN-DIVIDES)
(DISABLE TIMES)
(DEFN
CRYPT
(M E N)
(IF
(ZEROP E)
1
(IF (EVEN E)
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2)
N))
N)
(REMAINDER (TIMES M
(REMAINDER
(SQUARE (CRYPT M (QUOTIENT E 2)
N))
N))
N))))
(PROVE-LEMMA TIMES-MOD-1 (REWRITE)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y)
N)))
(PROVE-LEMMA TIMES-MOD-2 (REWRITE)
(EQUAL (REMAINDER (TIMES A
(TIMES B
(REMAINDER Y N)))
N)
(REMAINDER (TIMES A B Y)
N))
((USE (TIMES-MOD-1 (X (TIMES A B))))
(DISABLE TIMES-MOD-1)))
(PROVE-LEMMA CRYPT-CORRECT (REWRITE)
(IMPLIES (NOT (EQUAL N 1))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E)
N))))
(PROVE-LEMMA TIMES-MOD-3 (REWRITE)
(EQUAL (REMAINDER (TIMES (REMAINDER A N)
B)
N)
(REMAINDER (TIMES A B)
N)))
(PROVE-LEMMA REMAINDER-EXP-LEMMA (REWRITE)
(IMPLIES (EQUAL (REMAINDER Y A)
(REMAINDER Z A))
(EQUAL (EQUAL (REMAINDER (TIMES X Y)
A)
(REMAINDER (TIMES X Z)
A))
T)))
(PROVE-LEMMA REMAINDER-EXP (REWRITE)
(EQUAL (REMAINDER (EXP (REMAINDER A N)
I)
N)
(REMAINDER (EXP A I)
N)))
(PROVE-LEMMA EXP-MOD-IS-1 (REWRITE)
(IMPLIES (EQUAL (REMAINDER (EXP M J)
P)
1)
(EQUAL (REMAINDER (EXP M (TIMES I J))
P)
1))
((USE (EXP-EXP (I M)
(J J)
(K I))
(REMAINDER-EXP (A (EXP M J))
(N P)))
(DISABLE EXP-EXP REMAINDER-EXP)))
(DEFN PDIFFERENCE (A B)
(IF (LESSP A B)
(DIFFERENCE B A)
(DIFFERENCE A B))
NIL
; We wish to teach the system the trick of proving that A mod p = B mod p by
; considering whether p A-B. If we used DIFFERENCE we would have to split on
; whether A<B. So we introduce PDIFFERENCE that contains that split. Then
; we prove the necessary facts about TIMES, REMAINDER and PDIFFERENCE. During
; these proofs the case splits on A<B arise. But the case splits do not arise
; in the statements of the lemmas and so don't arise when we try to apply
; them. After proving what we need about PDIFFERENCE we disable it.
)
(PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PDIFFERENCE (REWRITE)
(EQUAL (TIMES M (PDIFFERENCE A B))
(PDIFFERENCE (TIMES M A)
(TIMES M B))))
(PROVE-LEMMA EQUAL-MODS-TRICK-1 (REWRITE)
(IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B)
P)
0)
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T)))
(PROVE-LEMMA EQUAL-MODS-TRICK-2 (REWRITE)
(IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER (PDIFFERENCE A B)
P)
0))
((DISABLE DIFFERENCE-ELIM)))
(DISABLE PDIFFERENCE)
(PROVE-LEMMA PRIME-KEY-TRICK (REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER (TIMES M A)
P)
(REMAINDER (TIMES M B)
P))
(NOT (EQUAL (REMAINDER M P)
0))
(PRIME P))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T))
((USE (PRIME-KEY-REWRITE (A M)
(B (PDIFFERENCE A B)))
(EQUAL-MODS-TRICK-2 (A (TIMES M A))
(B (TIMES M B))))
(DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2)))
(PROVE-LEMMA PRODUCT-DIVIDES-LEMMA (REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z)
0)
(EQUAL (REMAINDER (TIMES Y X)
(TIMES Y Z))
0)))
(PROVE-LEMMA PRODUCT-DIVIDES (REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X P)
0)
(EQUAL (REMAINDER X Q)
0)
(PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q))
0)))
(PROVE-LEMMA THM-53-SPECIALIZED-TO-PRIMES NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q))))
NIL
; The proof of this consists merely of applying trick 1 to backwards chain
; from A mod PQ = B mod PQ to PQ A-B, then use PRODUCT-DIVIDES to back up to
; P A-B and Q A-B, and then use trick 2 to come back to A mod P = B mod P.
)
(PROVE-LEMMA COROLLARY-53 (REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q))
B)
T))
((USE (THM-53-SPECIALIZED-TO-PRIMES))
(DISABLE THM-53-SPECIALIZED-TO-PRIMES)))
(PROVE-LEMMA THM-55-SPECIALIZED-TO-PRIMES (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X)
P)
(REMAINDER (TIMES M Y)
P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))))
(PROVE-LEMMA COROLLARY-55 (REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M X)
P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P)
0)
(EQUAL (REMAINDER X P)
1))))
((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1)))
(DISABLE THM-55-SPECIALIZED-TO-PRIMES)))
(DEFN ALL-DISTINCT (L)
(IF (NLISTP L)
T
(AND (NOT (MEMBER (CAR L)
(CDR L)))
(ALL-DISTINCT (CDR L)))))
(DEFN ALL-LESSEQP (L N)
(IF (NLISTP L)
T
(AND (NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L)
N))))
(DEFN ALL-NON-ZEROP (L)
(IF (NLISTP L)
T
(AND (NOT (ZEROP (CAR L)))
(ALL-NON-ZEROP (CDR L)))))
(DEFN POSITIVES (N)
(IF (ZEROP N)
NIL
(CONS N (POSITIVES (SUB1 N)))))
(PROVE-LEMMA LISTP-POSITIVES (REWRITE)
(EQUAL (LISTP (POSITIVES N))
(NOT (ZEROP N))))
(PROVE-LEMMA CAR-POSITIVES (REWRITE)
(EQUAL (CAR (POSITIVES N))
(IF (ZEROP N)
0 N)))
(PROVE-LEMMA MEMBER-POSITIVES (REWRITE)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X)
F
(LESSP X (ADD1 N)))))
(PROVE-LEMMA ALL-NON-ZEROP-DELETE (REWRITE)
(IMPLIES (ALL-NON-ZEROP L)
(ALL-NON-ZEROP (DELETE X L))))
(PROVE-LEMMA ALL-DISTINCT-DELETE (REWRITE)
(IMPLIES (ALL-DISTINCT L)
(ALL-DISTINCT (DELETE X L))))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-1 (REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N)
L)
N)))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-2 (REWRITE)
(IMPLIES (AND (NOT (MEMBER (ADD1 N)
X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)))
(PROVE-LEMMA PERM-MEMBER (REWRITE)
(IMPLIES (AND (PERM A B)
(MEMBER X A))
(MEMBER X B)))
(DEFN PIGEON-HOLE-INDUCTION (L)
(IF (LISTP L)
(IF (MEMBER (LENGTH L)
L)
(PIGEON-HOLE-INDUCTION (DELETE (LENGTH L)
L))
(PIGEON-HOLE-INDUCTION (CDR L)))
T))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE NIL
(IMPLIES (AND (ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L))
L))
((INDUCT (PIGEON-HOLE-INDUCTION L)))
; We have proved this theorem without this induction hint, but that proof
; requires many more lemmas. This is a good example of a theorem whose
; induction is not suggested by any term in the theorem.
)
(PROVE-LEMMA PERM-TIMES-LIST NIL
(IMPLIES (PERM L1 L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))))
(PROVE-LEMMA TIMES-LIST-POSITIVES (REWRITE)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N)))
(PROVE-LEMMA TIMES-LIST-EQUAL-FACT (REWRITE)
(IMPLIES (PERM (POSITIVES N)
L)
(EQUAL (TIMES-LIST L)
(FACT N)))
((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
(L2 L)))
(DISABLE PERM-TIMES-LIST)))
(PROVE-LEMMA PRIME-FACT (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N)
P)
0)))
((INDUCT (FACT N))))
(DEFN S (N M P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES M N)
P)
(S (SUB1 N)
M P))))
(PROVE-LEMMA REMAINDER-TIMES-LIST-S NIL
(EQUAL (REMAINDER (TIMES-LIST (S N M P))
P)
(REMAINDER (TIMES (FACT N)
(EXP M N))
P)))
(PROVE-LEMMA ALL-DISTINCT-S-LEMMA (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1)
P)
(S N2 M P))))
((INDUCT (S N2 M P))))
(PROVE-LEMMA ALL-DISTINCT-S (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(LESSP N P))
(ALL-DISTINCT (S N M P))))
(PROVE-LEMMA ALL-NON-ZEROP-S (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))))
(PROVE-LEMMA ALL-LESSEQP-S (REWRITE)
(IMPLIES (NOT (ZEROP P))
(ALL-LESSEQP (S N M P)
(SUB1 P))))
(PROVE-LEMMA LENGTH-S (REWRITE)
(EQUAL (LENGTH (S N M P))
(FIX N)))
(PROVE-LEMMA FERMAT-THM (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P)
0)))
(EQUAL (REMAINDER (EXP M (SUB1 P))
P)
1))
((USE (PIGEON-HOLE-PRINCIPLE (L (S (SUB1 P)
M P)))
(REMAINDER-TIMES-LIST-S (N (SUB1 P))))
(DISABLE PIGEON-HOLE-PRINCIPLE
REMAINDER-TIMES-LIST-S)))
(PROVE-LEMMA
CRYPT-INVERTS-STEP-1 NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M
(TIMES K
(SUB1 P))))
P)
(REMAINDER M P))))
(PROVE-LEMMA
CRYPT-INVERTS-STEP-1A
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M
(TIMES K
(SUB1 P)
(SUB1 Q))))
P)
(REMAINDER M P)))
((USE (CRYPT-INVERTS-STEP-1 (K (TIMES K (SUB1 Q)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
(PROVE-LEMMA
CRYPT-INVERTS-STEP-1B
(REWRITE)
(IMPLIES (PRIME Q)
(EQUAL (REMAINDER (TIMES M (EXP M
(TIMES K
(SUB1 P)
(SUB1 Q))))
Q)
(REMAINDER M Q)))
((USE (CRYPT-INVERTS-STEP-1 (P Q)
(K (TIMES K (SUB1 P)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
(PROVE-LEMMA CRYPT-INVERTS-STEP-2 (REWRITE)
(IMPLIES
(AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED (TIMES (SUB1 P)
(SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED)
(TIMES P Q))
M)))
(PROVE-LEMMA CRYPT-INVERTS NIL
(IMPLIES
(AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P)
(SUB1 Q)))
1))
(EQUAL (CRYPT (CRYPT M E N)
D N)
M))
NIL))
NIL "RSA")
;;; "WILSON"
(PROVEALL
'((NOTE-LIB "RSA.LIB" "RSA.LISP")
(DEFN INVERSE (J P)
(IF (EQUAL P 2)
(REMAINDER J 2)
(REMAINDER (EXP J (DIFFERENCE P 2))
P)))
(PROVE-LEMMA INVERSE-INVERTS-LEMMA (REWRITE)
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P)
J)
P)
(REMAINDER (EXP J (SUB1 P))
P))))
(PROVE-LEMMA INVERSE-INVERTS (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P)
J)
P)
1))
((USE (INVERSE-INVERTS-LEMMA))
(DISABLE INVERSE)))
(PROVE-LEMMA INVERSE-IS-UNIQUE (REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL 1 (REMAINDER (TIMES M X)
P)))
(EQUAL (INVERSE M P)
(REMAINDER X P)))
((USE (INVERSE-INVERTS (J M))
(THM-55-SPECIALIZED-TO-PRIMES
(Y (INVERSE M P))))))
(PROVE-LEMMA S-P-I-I-LEMMA1 (REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N)
(SUB1 N))
(PLUS 1 (TIMES N
(SUB1 (SUB1 N)))))))
(PROVE-LEMMA S-P-I-I-LEMMA2 (REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (SUB1 N)
(SUB1 N))
N)
1))
((USE (S-P-I-I-LEMMA1)
(REMAINDER-PLUS-TIMES-2
(J N)
(X 1)
(I (SUB1 (SUB1 N)))))
(DISABLE S-P-I-I-LEMMA1 REMAINDER-PLUS-TIMES-2)))
(PROVE-LEMMA SUB1-P-IS-INVOLUTION (REWRITE)
(IMPLIES (PRIME P)
(EQUAL (INVERSE (SUB1 P)
P)
(SUB1 P)))
((USE (INVERSE-IS-UNIQUE (M (SUB1 P))
(X (SUB1 P))))
(DISABLE INVERSE)))
(PROVE-LEMMA N-O-I-LEMMA1 (REWRITE)
(EQUAL (DIFFERENCE (TIMES X X)
1)
(TIMES (ADD1 X)
(SUB1 X))))
(PROVE-LEMMA
N-O-I-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (DIFFERENCE (TIMES J J)
1)
P)
0))
(OR (EQUAL (REMAINDER (ADD1 J)
P)
0)
(EQUAL (REMAINDER (SUB1 J)
P)
0))))
(PROVE-LEMMA N-O-I-LEMMA3 (REWRITE)
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P)
1))
(EQUAL (REMAINDER (SUB1 A)
P)
0))
((USE (EQUAL-MODS-TRICK-2 (B 1)))
(DISABLE N-O-I-LEMMA1)))
(PROVE-LEMMA N-O-I-LEMMA4 (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0))
(EQUAL (INVERSE J P)
J))
(OR (EQUAL (REMAINDER (ADD1 J)
P)
0)
(EQUAL (REMAINDER (SUB1 J)
P)
0)))
((USE (INVERSE-INVERTS)
(N-O-I-LEMMA2))
(DISABLE INVERSE N-O-I-LEMMA1)))
(PROVE-LEMMA NO-OTHER-INVOLUTIONS (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P))
(LESSP 1 J))
(NOT (EQUAL (INVERSE J P)
J)))
((USE (N-O-I-LEMMA4))
(DISABLE INVERSE)))
(PROVE-LEMMA I-O-I-LEMMA NIL
(EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
(DIFFERENCE P 2)))
(TIMES (DIFFERENCE P 3)
(SUB1 P))))
(PROVE-LEMMA INVERSE-OF-INVERSE (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(EQUAL (INVERSE (INVERSE J P)
P)
(REMAINDER J P)))
((USE (I-O-I-LEMMA)
(EXP-MOD-IS-1 (M J)
(J (SUB1 P))
(I (DIFFERENCE P 3))))))
(PROVE-LEMMA N-Z-I-LEMMA (REWRITE)
(IMPLIES (AND (ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P)
0)))
(PROVE-LEMMA NON-ZEROP-INVERSE (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0)))
(NOT (ZEROP (INVERSE J P))))
((USE (N-Z-I-LEMMA (I (INVERSE J P)))
(INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
(PROVE-LEMMA B-I-LEMMA2 (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P)
0))
(EQUAL (INVERSE J P)
(SUB1 P)))
(EQUAL (REMAINDER J P)
(SUB1 P)))
((USE (INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
(PROVE-LEMMA B-I-LEMMA1 NIL (IMPLIES (LESSP 1 P)
(LEQ (INVERSE J P)
(SUB1 P))))
(PROVE-LEMMA BOUNDED-INVERSE (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P)
(SUB1 P)))
((USE (B-I-LEMMA1)
(B-I-LEMMA2))
(DISABLE INVERSE)))
(DEFN
INVERSE-LIST
(I P)
(IF (ZEROP I)
NIL
(IF (EQUAL I 1)
(CONS 1 NIL)
(IF (MEMBER I (INVERSE-LIST (SUB1 I)
P))
(INVERSE-LIST (SUB1 I)
P)
(CONS I (CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I)
P)))))))
(PROVE-LEMMA ALL-NON-ZEROP-INVERSE-LIST (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST I P)))
((USE (NON-ZEROP-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
(PROVE-LEMMA BOUNDED-INVERSE-LIST (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(EQUAL J (DIFFERENCE P 2)))
(ALL-LESSEQP (INVERSE-LIST I P)
J))
((USE (BOUNDED-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
(PROVE-LEMMA SUBSETP-POSITIVES (REWRITE)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P)))
(PROVE-LEMMA INVERSE-1 (REWRITE)
(IMPLIES (LESSP 1 P)
(EQUAL (INVERSE 1 P)
1)))
(PROVE-LEMMA A-D-I-L-LEMMA1 (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0))
(LESSP I P)
(MEMBER J (INVERSE-LIST I P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
(PROVE-LEMMA A-D-I-L-LEMMA2 (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0))
(NOT (EQUAL (REMAINDER J P)
0))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE)
(A-D-I-L-LEMMA1 (J (INVERSE J P))))
(DISABLE INVERSE INVERSE-LIST INVERSE-OF-INVERSE
A-D-I-L-LEMMA1)))
(PROVE-LEMMA A-D-I-L-LEMMA3 (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(ALL-DISTINCT
(INVERSE-LIST (SUB1 I)
P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA2 (J I)
(I (SUB1 I)))
(NO-OTHER-INVOLUTIONS (J I)))
(DISABLE INVERSE)))
(PROVE-LEMMA ALL-DISTINCT-INVERSE-LIST (REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA3))
(INDUCT (POSITIVES I))
(DISABLE INVERSE)))
(PROVE-LEMMA T-I-L-LEMMA1 (REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES A B)
P)
1)
(EQUAL (REMAINDER (TIMES A (TIMES B C))
P)
(REMAINDER C P)))
((USE (TIMES-MOD-3 (A (TIMES A B))
(B C)
(N P)))
(DISABLE TIMES-MOD-3)))
(PROVE-LEMMA
T-I-L-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES I (INVERSE I P))
P)
1)
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST
(INVERSE-LIST (SUB1 I)
P))
P)))
((USE (T-I-L-LEMMA1 (A I)
(B (INVERSE I P))
(C (TIMES-LIST (INVERSE-LIST (SUB1 I)
P)))))
(DISABLE T-I-L-LEMMA1 INVERSE INVERSE-INVERTS)))
(PROVE-LEMMA
T-I-L-LEMMA3
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P)
0)))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST
(INVERSE-LIST (SUB1 I)
P))
P)))
((USE (INVERSE-INVERTS (J I)))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST REMAINDER PRIME)))
(PROVE-LEMMA T-I-L-LEMMA4 (REWRITE)
(IMPLIES (LEQ I 1)
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)))
(PROVE-LEMMA TIMES-INVERSE-LIST (REWRITE)
(IMPLIES
(AND (PRIME P)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST
(INVERSE-LIST I P))
P)
1))
((USE (T-I-L-LEMMA3)
(T-I-L-LEMMA4))
(INDUCT (POSITIVES I))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST
T-I-L-LEMMA3 T-I-L-LEMMA4)))
(PROVE-LEMMA DELETE-X-LEAVE-A (REWRITE)
(IMPLIES (AND (MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))))
(PROVE-LEMMA DELETE-MEMBER-LEAVE-SUBSET (REWRITE)
(IMPLIES (AND (SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))))
(PROVE-LEMMA ALL-LESSEQP-DELETE (REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L)
(SUB1 N))))
(PROVE-LEMMA POSITIVES-BOUNDED (REWRITE)
(IMPLIES (LESSP N M)
(NOT (MEMBER M (POSITIVES N)))))
(PROVE-LEMMA SUBSETP-POSITIVES-DELETE (REWRITE)
(IMPLIES (SUBSETP (POSITIVES N)
L)
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L))))
(PROVE-LEMMA NONZEROP-LESSEQP-ZERO (REWRITE)
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))))
(DEFN PIGEONHOLE2-INDUCTION (L N)
(IF (ZEROP N)
T
(PIGEONHOLE2-INDUCTION (DELETE N L)
(SUB1 N))))
(PROVE-LEMMA PIGEONHOLE2 (REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N)
L))
(PERM (POSITIVES N)
L))
((INDUCT (PIGEONHOLE2-INDUCTION L N))))
(PROVE-LEMMA PERM-POSITIVES-INVERSE-LIST (REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(PERM (POSITIVES I)
(INVERSE-LIST I P))))
(PROVE-LEMMA INVERSE-LIST-FACT (REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
((USE (TIMES-LIST-EQUAL-FACT
(N I)
(L (INVERSE-LIST I P))))
(DISABLE INVERSE-LIST)))
(PROVE-LEMMA W-T-LEMMA (REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT I)
P)
1))
((USE (TIMES-INVERSE-LIST))))
(PROVE-LEMMA WILSON-THM NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (FACT (SUB1 P))
P)
(SUB1 P)))
((USE (W-T-LEMMA (I (SUB1 (SUB1 P))))
(THM-55-SPECIALIZED-TO-PRIMES
(M (SUB1 P))
(X (FACT (SUB1 (SUB1 P))))
(Y 1)))
(DISABLE W-T-LEMMA THM-55-SPECIALIZED-TO-PRIMES))))
NIL "WILSON")
;;; "GAUSS"
(PROVEALL
'((NOTE-LIB "WILSON.LIB" "WILSON.LISP")
(DEFN SQUARES
(N P)
(IF (ZEROP N)
(LIST 0)
(CONS (REMAINDER (TIMES N N) P) (SQUARES (SUB1 N) P))))
(DEFN RESIDUE
(A P)
(AND (NOT (DIVIDES P A))
(MEMBER (REMAINDER A P) (SQUARES P P))))
(PROVE-LEMMA ALL-SQUARES-1
NIL
(IMPLIES (AND (NOT (ZEROP P))
(LEQ M N))
(MEMBER (REMAINDER (TIMES M M) P)
(SQUARES N P))))
(PROVE-LEMMA ALL-SQUARES-2
NIL
(EQUAL (REMAINDER (TIMES Y Y) P)
(REMAINDER (TIMES (REMAINDER Y P)
(REMAINDER Y P))
P))
((USE (TIMES-MOD-1 (X Y) (N P))
(TIMES-MOD-3 (B (REMAINDER Y P)) (A Y) (N P)))
(DISABLE TIMES-MOD-1 TIMES-MOD-3)))
(PROVE-LEMMA ALL-SQUARES
(REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (MEMBER X (SQUARES P P))))
(NOT (EQUAL X (REMAINDER (TIMES Y Y) P))))
((USE (ALL-SQUARES-1 (N P) (M (REMAINDER Y P)))
(ALL-SQUARES-2))
(DISABLE TIMES-MOD-1 TIMES-MOD-3)))
(PROVE-LEMMA EULER-1-1
NIL
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))))
(PROVE-LEMMA
EULER-1-2
NIL
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (EXP (TIMES I I) (QUOTIENT P 2)) (EXP I (SUB1 P))))
((USE (EXP-EXP (J 2) (K (QUOTIENT P 2))) (EULER-1-1))
(DISABLE EXP-EXP)))
(PROVE-LEMMA EULER-1-3
NIL
(IMPLIES (EQUAL (REMAINDER A P) (REMAINDER B P))
(EQUAL (REMAINDER (EXP A C) P)
(REMAINDER (EXP B C) P)))
((USE (REMAINDER-EXP (I C) (N P))
(REMAINDER-EXP (A B) (I C) (N P)))
(DISABLE REMAINDER-EXP)))
(PROVE-LEMMA EULER-1-4
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P I)))
(EQUAL (REMAINDER (EXP (TIMES I I)
(QUOTIENT P 2))
P)
1))
((USE (EULER-1-2)) (DISABLE LESSP-REMAINDER-DIVISOR
PRIME)))
(PROVE-LEMMA
EULER-1-5
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P)))
(NOT (DIVIDES P I)))
((USE (PRIME-KEY-REWRITE (A I) (B I))) (DISABLE PRIME-KEY-REWRITE
PRIME)))
(PROVE-LEMMA EULER-1-6
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(EQUAL (REMAINDER A P)
(REMAINDER (TIMES I I) P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
1))
((USE (EULER-1-4)
(EULER-1-5)
(EULER-1-3 (B (TIMES I I)) (C (QUOTIENT P 2))))
(DISABLE PRIME
LESSP-REMAINDER-DIVISOR
B-ILEMMA2
LESSP
SUB1-NNUMBERP
REMAINDER-0-CROCK
REMAINDER)))
(PROVE-LEMMA EULER-1-7
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(MEMBER (REMAINDER A P) (SQUARES I P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
1))
((USE (EULER-1-6)) (INDUCT (SQUARES I P))
(DISABLE PRIME
REMAINDER
LESSP-REMAINDER-DIVISOR)))
(PROVE-LEMMA EULER-1
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(RESIDUE A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
1))
((DISABLE PRIME)))
(DEFN COMPLEMENT (J A P) (REMAINDER (TIMES (INVERSE J P) A) P))
(TOGGLE G0219 INVERSE T)
(PROVE-LEMMA COMPLEMENT-WORKS
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J)))
(EQUAL (REMAINDER
(TIMES J
(COMPLEMENT J A P))
P)
(REMAINDER A P)))
((USE (INVERSE-INVERTS)
(TIMES-MOD-3 (A (TIMES J (INVERSE J P)))
(B A)
(N P)))
(DISABLE INVERSE-INVERTS TIMES-MOD-3 PRIME)))
(PROVE-LEMMA BOUNDED-COMPLEMENT
(REWRITE)
(IMPLIES (NOT (ZEROP P)) (LESSP (COMPLEMENT J A P) P)))
(TOGGLE COMPLEMENT-OFF COMPLEMENT T)
(PROVE-LEMMA NON-ZEROP-COMPLEMENT
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A)))
(NOT (ZEROP (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS)) (DISABLE COMPLEMENT-WORKS
PRIME)))
(PROVE-LEMMA
COMPLEMENT-IS-UNIQUE
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P)))
(EQUAL (COMPLEMENT J A P) (REMAINDER X P)))
((USE (COMPLEMENT-WORKS)
(THM-55-SPECIALIZED-TO-PRIMES (M J) (Y (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-WORKS THM-55-SPECIALIZED-TO-PRIMES PRIME)))
(TOGGLE SQUARES-OFF SQUARES T)
(PROVE-LEMMA NO-SELF-COMPLEMENT
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(NOT (EQUAL J (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS)
(ALL-SQUARES (X (REMAINDER A P)) (Y J)))
(DISABLE COMPLEMENT-WORKS ALL-SQUARES PRIME1)))
(PROVE-LEMMA COMPLEMENT-OF-COMPLEMENT
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P J))
(NOT (DIVIDES P A)))
(EQUAL (COMPLEMENT (COMPLEMENT J A P) A P)
(REMAINDER J P)))
((USE (COMPLEMENT-WORKS)
(COMPLEMENT-IS-UNIQUE (J (COMPLEMENT J A P))
(X J)))
(DISABLE COMPLEMENT-WORKS COMPLEMENT-IS-UNIQUE)))
(DEFN COMP-LIST
(I A P)
(IF (ZEROP I)
NIL
(IF (MEMBER I (COMP-LIST (SUB1 I) A P))
(COMP-LIST (SUB1 I) A P)
(CONS I
(CONS (COMPLEMENT I A P)
(COMP-LIST (SUB1 I) A P))))))
(PROVE-LEMMA
ALL-NON-ZEROP-COMP-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A)))
(ALL-NON-ZEROP (COMP-LIST I A P)))
((USE (NON-ZEROP-COMPLEMENT (J I))) (INDUCT (COMP-LIST I A P))))
(PROVE-LEMMA
BOUNDED-COMP-LIST
(REWRITE)
(IMPLIES (LESSP I P) (ALL-LESSEQP (COMP-LIST I A P) (SUB1 P)))
((USE (BOUNDED-COMPLEMENT (J I))) (INDUCT (COMP-LIST I A P))))
(PROVE-LEMMA SUBSETP-POSITIVES-COMP-LIST
(REWRITE)
(SUBSETP (POSITIVES N) (COMP-LIST N A P)))
(PROVE-LEMMA
COMP-LIST-CLOSED-1
NIL
(IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(LESSP I P)
(NOT (DIVIDES P A))
(MEMBER J (COMP-LIST I A P)))
(MEMBER (COMPLEMENT J A P) (COMP-LIST I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT (J I)))
(INDUCT (COMP-LIST I A P))
(DISABLE COMPLEMENT-OF-COMPLEMENT)))
(PROVE-LEMMA COMP-LIST-CLOSED-2
NIL
(IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(NOT (ZEROP J))
(LESSP I P)
(LESSP J P)
(NOT (DIVIDES P A))
(MEMBER (COMPLEMENT J A P)
(COMP-LIST I A P)))
(MEMBER J (COMP-LIST I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT)
(COMP-LIST-CLOSED-1 (J (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-OF-COMPLEMENT COMP-LIST)))
(PROVE-LEMMA ALL-DISTINCT-COMP-LIST-1
NIL
(IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P))
(ALL-DISTINCT
(COMP-LIST (SUB1 I) A P)))
(ALL-DISTINCT (COMP-LIST I A P)))
((USE (COMP-LIST-CLOSED-2 (J I) (I (SUB1 I)))
(NO-SELF-COMPLEMENT (J I)))
(DISABLE PRIME)))
(PROVE-LEMMA
ALL-DISTINCT-COMP-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(ALL-DISTINCT (COMP-LIST I A P)))
((USE (ALL-DISTINCT-COMP-LIST-1)) (INDUCT (POSITIVES I))
(DISABLE PRIME)))
(PROVE-LEMMA PERM-POSITIVES-COMP-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(PERM (POSITIVES (SUB1 P))
(COMP-LIST (SUB1 P) A P))))
(PROVE-LEMMA COMP-LIST-FACT
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (TIMES-LIST (COMP-LIST (SUB1 P) A P))
(FACT (SUB1 P))))
((USE (TIMES-LIST-EQUAL-FACT (N (SUB1 P))
(L (COMP-LIST (SUB1 P)
A
P))))
(DISABLE TIMES-LIST-EQUAL-FACT COMP-LIST)))
(PROVE-LEMMA
TIMES-MOD-4
NIL
(IMPLIES (EQUAL (REMAINDER (TIMES I J) P) (REMAINDER A P))
(EQUAL (REMAINDER (TIMES I (TIMES J K)) P)
(REMAINDER (TIMES A (REMAINDER K P)) P)))
((USE (TIMES-MOD-3 (A (TIMES I J)) (B K) (N P)))
(DISABLE TIMES-MOD-3)))
(PROVE-LEMMA
TIMES-COMP-LIST-1
NIL
(IMPLIES
(AND (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P)
(REMAINDER A P))
(NOT (ZEROP I))
(NOT (MEMBER I (COMP-LIST (SUB1 I) A P))))
(EQUAL
(REMAINDER (TIMES-LIST (COMP-LIST I A P)) P)
(REMAINDER (TIMES A
(REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I)
A
P))
P))
P)))
((USE (TIMES-MOD-4 (J (COMPLEMENT I A P))
(K (TIMES-LIST (COMP-LIST (SUB1 I) A P)))))
(DISABLE COMPLEMENT-WORKS)))
(PROVE-LEMMA
TIMES-COMP-LIST-2
NIL
(IMPLIES
(AND (PRIME P)
(NOT (DIVIDES P I))
(NOT (MEMBER I (COMP-LIST (SUB1 I) A P))))
(EQUAL
(REMAINDER (TIMES-LIST (COMP-LIST I A P)) P)
(REMAINDER (TIMES A
(REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I)
A
P))
P))
P)))
((USE (TIMES-COMP-LIST-1) (COMPLEMENT-WORKS (J I)))
(DISABLE COMPLEMENT-WORKS COMP-LIST TIMES-LIST PRIME)))
(PROVE-LEMMA QUOTIENT-PLUS-1
NIL
(IMPLIES (AND (NOT (ZEROP N))
(NUMBERP X)
(EQUAL Y (PLUS X N)))
(EQUAL (QUOTIENT Y N) (ADD1 (QUOTIENT X N)))))
(PROVE-LEMMA
TIMES-COMP-LIST-3
NIL
(IMPLIES (AND (NOT (ZEROP I))
(NOT (MEMBER I (COMP-LIST (SUB1 I) A P))))
(EQUAL (QUOTIENT (LENGTH (COMP-LIST I A P)) 2)
(ADD1 (QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A
P))
2))))
((USE (QUOTIENT-PLUS-1 (X (LENGTH (COMP-LIST (SUB1 I) A P)))
(Y (LENGTH (COMP-LIST I A P)))
(N 2)))))
(PROVE-LEMMA
TIMES-COMP-LIST-4
NIL
(IMPLIES
(AND
(PRIME P)
(NOT (ZEROP I))
(LESSP I P)
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST (SUB1 I) A P)) P)
(REMAINDER (EXP A
(QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A
P))
2))
P)))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P)) P)
(REMAINDER (EXP A
(QUOTIENT (LENGTH (COMP-LIST I A P)) 2))
P)))
((USE
(TIMES-COMP-LIST-2)
(TIMES-COMP-LIST-3)
(TIMES-MOD-1 (X A)
(Y (EXP A
(QUOTIENT (LENGTH (COMP-LIST (SUB1 I)
A
P))
2)))
(N P)))
(DISABLE PRIME TIMES-MOD-1 TIMES-LIST)))
(PROVE-LEMMA
TIMES-COMP-LIST-5
NIL
(IMPLIES (ZEROP I)
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P)) P)
(REMAINDER (EXP A
(QUOTIENT (LENGTH (COMP-LIST I
A
P))
2))
P))))
(PROVE-LEMMA
TIMES-COMP-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (COMP-LIST I A P)) P)
(REMAINDER (EXP A
(QUOTIENT (LENGTH (COMP-LIST I
A
P))
2))
P)))
((USE (TIMES-COMP-LIST-4) (TIMES-COMP-LIST-5))
(INDUCT (POSITIVES I))
(DISABLE PRIME REMAINDER TIMES-LIST COMP-LIST QUOTIENT LENGTH)))
(PROVE-LEMMA SUB1-LENGTH-DELETE
(REWRITE)
(IMPLIES (MEMBER X B)
(EQUAL (LENGTH (DELETE X B))
(SUB1 (LENGTH B)))))
(PROVE-LEMMA EQUAL-LENGTH-PERM
NIL
(IMPLIES (PERM A B) (EQUAL (LENGTH A) (LENGTH B)))
((INDUCT (PERM A B))))
(PROVE-LEMMA LENGTH-POSITIVES
(REWRITE)
(EQUAL (LENGTH (POSITIVES N)) (FIX N))
((INDUCT (POSITIVES N))))
(PROVE-LEMMA
EULER-2-1
NIL
(IMPLIES
(AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (REMAINDER (EXP A
(QUOTIENT (LENGTH (COMP-LIST (SUB1 P)
A
P))
2))
P)
(SUB1 P)))
((USE (TIMES-COMP-LIST (I (SUB1 P)))
(COMP-LIST-FACT)
(WILSON-THM))
(DISABLE TIMES-COMP-LIST COMP-LIST-FACT)))
(PROVE-LEMMA EULER-2-2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (LENGTH (COMP-LIST (SUB1 P) A P))
(SUB1 P)))
((USE (EQUAL-LENGTH-PERM (A (POSITIVES (SUB1 P)))
(B (COMP-LIST
(SUB1 P) A P)))
(PERM-POSITIVES-COMP-LIST))
(DISABLE EQUAL-LENGTH-PERM
PERM-POSITIVES-COMP-LIST)))
(PROVE-LEMMA EULER-2-3
NIL
(IMPLIES (NOT (ZEROP P))
(EQUAL (DIVIDES 2 P)
(NOT (DIVIDES 2 (SUB1 P)))))
((INDUCT (ODD P))))
(PROVE-LEMMA EULER-2-4
(REWRITE)
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (QUOTIENT (SUB1 P) 2)
(QUOTIENT P 2)))
((USE (EULER-2-3)
(REMAINDER-QUOTIENT (X P) (Y 2))
(REMAINDER-QUOTIENT (X (SUB1 P)) (Y 2)))
(DISABLE RES-REM-2LEMMA3 REMAINDER-QUOTIENT)))
(PROVE-LEMMA EULER-2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
(SUB1 P)))
((USE (EULER-2-1)) (DISABLE EULER-2-1
PRIME
DIVIDES
RESIDUE
EXP
QUOTIENT
LENGTH
COMP-LIST)))
(DEFN RES1
(N A P)
(IF (ZEROP N)
T
(IF (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(NOT (RES1 (SUB1 N) A P))
(RES1 (SUB1 N) A P))))
(DEFN REFLECT (X P) (DIFFERENCE P X))
(DEFN REFLECT-LIST
(N A P)
(IF (ZEROP N)
NIL
(IF (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(CONS (REFLECT (REMAINDER (TIMES A N) P) P)
(REFLECT-LIST (SUB1 N) A P))
(CONS (REMAINDER (TIMES A N) P)
(REFLECT-LIST (SUB1 N) A P)))))
(PROVE-LEMMA DIFF-MOD-1
(REWRITE)
(IMPLIES (LEQ B A)
(EQUAL (REMAINDER (DIFFERENCE A
(REMAINDER B
P))
P)
(REMAINDER (DIFFERENCE A B) P)))
((USE (REMAINDER-QUOTIENT (X B) (Y P))
(REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE A B))
(I (QUOTIENT B P))
(J P)))
(DISABLE REMAINDER-QUOTIENT
REMAINDER-PLUS-TIMES-1
REMAINDER-PLUS-TIMES-2)))
(PROVE-LEMMA REM-DIFF-TIMES
(REWRITE)
(IMPLIES (AND (LESSP X P)
(NOT (ZEROP X))
(NOT (ZEROP B)))
(EQUAL (REMAINDER (DIFFERENCE (TIMES B P) X)
P)
(DIFFERENCE P X)))
((USE (REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE P X))
(I (SUB1 B))
(J P)))
(DISABLE REMAINDER-PLUS-TIMES-1
REMAINDER-PLUS-TIMES-2)))
(PROVE-LEMMA
REFLECT-COMMUTES-WITH-TIMES-1
(REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES (REFLECT Y P) X) P)
(REMAINDER (REFLECT (REMAINDER (TIMES Y X) P) P)
P)))
((USE (DIFF-MOD-1 (A (TIMES P X)) (B (TIMES Y X)))
(LESSP-TIMES-CANCELLATION (Z X) (X Y) (Y P))
(REM-DIFF-TIMES (B X) (X (REMAINDER (TIMES Y X) P))))
(DISABLE LESSP-TIMES-CANCELLATION REM-DIFF-TIMES DIFF-MOD-1)))
(PROVE-LEMMA
REFLECT-COMMUTES-WITH-TIMES-2
(REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES X (REFLECT Y P)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES X Y) P) P)
P)))
((USE (REFLECT-COMMUTES-WITH-TIMES-1))
(DISABLE REFLECT-COMMUTES-WITH-TIMES-1 REFLECT)))
(PROVE-LEMMA
TIMES-EXP-FACT
(REWRITE)
(IMPLIES (NOT (ZEROP N))
(EQUAL (REMAINDER (TIMES (TIMES A N)
(TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))
P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P))))
(PROVE-LEMMA
REM-REFLECT-LIST-1
(REWRITE)
(IMPLIES
(AND (NOT (ZEROP P))
(NOT (ZEROP N))
(NOT (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N) A P))
P)
(REMAINDER (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)))
((USE
(REMAINDER-EXP-LEMMA (A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A
P)))
(Z (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT)))
(PROVE-LEMMA
REM-REFLECT-LIST-2
(REWRITE)
(IMPLIES
(AND (NOT (ZEROP P))
(NOT (ZEROP N))
(LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N) A P))
P)
(REMAINDER (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N) (FACT N))
P)
P)
P)))
((USE
(REMAINDER-EXP-LEMMA (A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N)
A
P)))
(Z (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT)))
(PROVE-LEMMA
REM-REFLECT-LIST-3
(REWRITE)
(IMPLIES
(AND
(NOT (ZEROP P))
(NOT (ZEROP N))
(NOT (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N) A P)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P)
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N) (FACT N))
P)
P)
P)))
((USE
(REMAINDER-EXP-LEMMA
(A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N) A P)))
(Z (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT)))
(PROVE-LEMMA
DOUBLE-REFLECT
(REWRITE)
(IMPLIES (LEQ A P)
(EQUAL (REMAINDER (REFLECT (REMAINDER (REFLECT A P) P) P)
P)
(REMAINDER A P))))
(PROVE-LEMMA
REM-REFLECT-LIST-4
(REWRITE)
(IMPLIES
(AND
(NOT (ZEROP P))
(NOT (ZEROP N))
(LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST (SUB1 N) A P)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P)
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)))
((USE
(REMAINDER-EXP-LEMMA
(A P)
(X (TIMES A N))
(Y (TIMES-LIST (REFLECT-LIST (SUB1 N) A P)))
(Z (REFLECT (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P)
P))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA REFLECT)))
(PROVE-LEMMA
REM-REFLECT-LIST-BASE-CASE
(REWRITE)
(IMPLIES (ZEROP N)
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P))))
(PROVE-LEMMA
REM-REFLECT-LIST
NIL
(IMPLIES
(NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECT-LIST N A P)) P)
(IF (RES1 N A P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)
(REMAINDER (REFLECT (REMAINDER (TIMES (EXP A N)
(FACT N))
P)
P)
P))))
((HANDS-OFF TIMES-LIST REFLECT-LIST QUOTIENT EXP FACT TIMES)
(DISABLE REFLECT)))
(PROVE-LEMMA LENGTH-REFLECT-LIST
(REWRITE)
(EQUAL (LENGTH (REFLECT-LIST N A P)) (FIX N))
((INDUCT (POSITIVES N))))
(PROVE-LEMMA ALL-LESSEQP-REFLECT-LIST-1
(REWRITE)
(IMPLIES (LESSP (QUOTIENT P 2) X)
(NOT (LESSP (QUOTIENT P 2) (REFLECT X P)))))
(PROVE-LEMMA ALL-LESSEQP-REFLECT-LIST
(REWRITE)
(ALL-LESSEQP (REFLECT-LIST N A P) (QUOTIENT P 2))
((DISABLE REFLECT)))
(PROVE-LEMMA ALL-NON-ZEROP-REFLECT-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LESSP B P))
(ALL-NON-ZEROP (REFLECT-LIST B A P)))
((INDUCT (REFLECT-LIST B A P)) (DISABLE PRIME1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-1
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J I)
(LESSP I P)
(NOT (DIVIDES P A)))
(NOT (EQUAL (REMAINDER (TIMES A I) P)
(REMAINDER (TIMES A J) P))))
((DISABLE PRIME)))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-2
(REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(LESSP X P)
(LESSP Y P))
(EQUAL (EQUAL (DIFFERENCE P X)
(DIFFERENCE P Y))
(EQUAL X Y))))
(PROVE-LEMMA NUMBERP-REMAINDER
(REWRITE)
(NUMBERP (REMAINDER A P)))
(PROVE-LEMMA
ALL-DISTINCT-REFLECT-LIST-3
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J I)
(LESSP I P)
(NOT (DIVIDES P A)))
(NOT (EQUAL (REFLECT (REMAINDER (TIMES A I) P) P)
(REFLECT (REMAINDER (TIMES A J) P) P))))
((USE (ALL-DISTINCT-REFLECT-LIST-1))
(HANDS-OFF DIFFERENCE REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECT-LIST-1 PRIME)))
(PROVE-LEMMA PLUS-MOD-1
(REWRITE)
(EQUAL (REMAINDER (PLUS (REMAINDER X P) Y) P)
(REMAINDER (PLUS X Y) P))
((USE (REMAINDER-QUOTIENT (Y P))
(REMAINDER-PLUS-TIMES-1 (J P)
(X (PLUS (REMAINDER X
P)
Y))
(I (QUOTIENT X P))))
(DISABLE REMAINDER-QUOTIENT
REMAINDER-QUOTIENT-ELIM
REMAINDER-PLUS-TIMES-1)))
(PROVE-LEMMA PLUS-MOD-2
(REWRITE)
(EQUAL (REMAINDER (PLUS Y (REMAINDER X P)) P)
(REMAINDER (PLUS X Y) P))
((USE (PLUS-MOD-1)) (DISABLE PLUS-MOD-1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-4
NIL
(IMPLIES (AND (EQUAL X (DIFFERENCE P Y))
(LESSP Y P))
(EQUAL (REMAINDER (PLUS X Y) P) 0)))
;; (SWAP-OUT "GAUSS-TEMP-LIB-1")
(MAKE-LIB "G-TEMP")
(NOTE-LIB "G-TEMP.LIB" "G-TEMP.LISP")
(PROVE-LEMMA
ALL-DISTINCT-REFLECT-LIST-5
NIL
(IMPLIES (AND (EQUAL (REMAINDER (TIMES A I) P)
(DIFFERENCE P (REMAINDER (TIMES A J) P)))
(NOT (ZEROP P)))
(EQUAL (REMAINDER (TIMES A (PLUS I J)) P) 0))
((USE (ALL-DISTINCT-REFLECT-LIST-4 (X (REMAINDER (TIMES A I) P))
(Y (REMAINDER (TIMES A J) P))))
))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-6
NIL
(IMPLIES (AND (LEQ I (QUOTIENT P 2))
(LESSP J I))
(AND (NOT (ZEROP (PLUS I J)))
(LESSP (PLUS I J) P))))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-7
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (EQUAL (REMAINDER (TIMES A I) P)
(REFLECT (REMAINDER (TIMES A J)
P)
P))))
((USE (ALL-DISTINCT-REFLECT-LIST-5)
(ALL-DISTINCT-REFLECT-LIST-6))
(HANDS-OFF DIFFERENCE TIMES PLUS)
(DISABLE PRIME1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST-8
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (EQUAL (REFLECT (REMAINDER (TIMES A I)
P)
P)
(REMAINDER (TIMES A J) P))))
((USE (ALL-DISTINCT-REFLECT-LIST-5 (J I) (I J))
(ALL-DISTINCT-REFLECT-LIST-6))
(HANDS-OFF TIMES DIFFERENCE)
(DISABLE PRIME1)))
(PROVE-LEMMA
ALL-DISTINCT-REFLECT-LIST-9
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (REMAINDER (TIMES A I) P)
(REFLECT-LIST J A P))))
((USE (ALL-DISTINCT-REFLECT-LIST-1))
(INDUCT (REFLECT-LIST J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 REFLECT ALL-DISTINCT-REFLECT-LIST-1)))
(PROVE-LEMMA
ALL-DISTINCT-REFLECT-LIST-10
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (REFLECT (REMAINDER (TIMES A I) P) P)
(REFLECT-LIST J A P))))
((USE (ALL-DISTINCT-REFLECT-LIST-3))
(INDUCT (REFLECT-LIST J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 REFLECT ALL-DISTINCT-REFLECT-LIST-3)))
(PROVE-LEMMA ALL-DISTINCT-REFLECT-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2)))
(ALL-DISTINCT (REFLECT-LIST I A P)))
((USE (ALL-DISTINCT-REFLECT-LIST-9 (J (SUB1 I)))
(ALL-DISTINCT-REFLECT-LIST-10 (J (SUB1 I))))
(INDUCT (REFLECT-LIST I A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECT-LIST-9
ALL-DISTINCT-REFLECT-LIST-10
PRIME
DIVIDES
REFLECT)))
(PROVE-LEMMA
TIMES-REFLECT-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)))
(EQUAL (TIMES-LIST (REFLECT-LIST (QUOTIENT P 2) A P))
(FACT (QUOTIENT P 2))))
((USE (PIGEON-HOLE-PRINCIPLE (L (REFLECT-LIST (QUOTIENT P 2)
A
P))))
(HANDS-OFF QUOTIENT REMAINDER)
(DISABLE PRIME1 REFLECT-LIST TIMES-LIST FACT)))
(PROVE-LEMMA PLUS-X-X-EVEN
(REWRITE)
(EQUAL (REMAINDER (PLUS X X) 2) 0))
(PROVE-LEMMA RES1-REM-1-1
NIL
(IMPLIES (AND (NOT (ZEROP X))
(NOT (DIVIDES 2 P)))
(NOT (EQUAL (REMAINDER (DIFFERENCE P X) P)
X)))
((USE (DIFFERENCE-ELIM (Y P)))))
(PROVE-LEMMA RES1-REM-1
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(RES1 (QUOTIENT P 2) A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
1))
((USE (REM-REFLECT-LIST (N (QUOTIENT P 2)))
(PRIME-KEY-TRICK (M (FACT (QUOTIENT P 2)))
(A (EXP A (QUOTIENT P 2)))
(B 1)))
(DISABLE PRIME-KEY-TRICK
LESSP-REMAINDER-DIVISOR
PRIME1)))
(PROVE-LEMMA REMAINDER-LESSP
NIL
(IMPLIES (LESSP A P) (EQUAL (REMAINDER A P) (FIX A))))
(PROVE-LEMMA
RES1-REM-2
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(NOT (RES1 (QUOTIENT P 2) A P)))
(NOT (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)))
((USE (REM-REFLECT-LIST (N (QUOTIENT P 2)))
(REMAINDER-EXP-LEMMA (A P)
(Y (EXP A (QUOTIENT P 2)))
(Z 1)
(X (FACT (QUOTIENT P 2))))
(RES1-REM-1-1 (X (REMAINDER (FACT (QUOTIENT P 2)) P)))
(REMAINDER-LESSP (A 1)))
(HANDS-OFF FACT EXP QUOTIENT REMAINDER REFLECT-LIST)
(DISABLE LESSP-REMAINDER-DIVISOR
PRIME1
DIFFERENCE
COROLLARY-55
REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA TWO-EVEN
NIL
(IMPLIES (NOT (DIVIDES 2 P))
(NOT (EQUAL (SUB1 P) 1)))
((INDUCT (ODD P))))
(PROVE-LEMMA GAUSS-LEMMA
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (DIVIDES 2 P)))
(EQUAL (RES1 (QUOTIENT P 2) A P)
(RESIDUE A P)))
((USE (EULER-1)
(EULER-2)
(RES1-REM-1)
(RES1-REM-2)
(TWO-EVEN))
(DISABLE EULER-1
EULER-2
QUOTIENT
EXP
RESIDUE
RES1
PRIME
DIVIDES)))
(DEFN PLUS-LIST
(L)
(IF (NLISTP L) 0 (PLUS (CAR L) (PLUS-LIST (CDR L)))))
(DEFN QUOT-LIST
(N A P)
(IF (ZEROP N)
NIL
(CONS (QUOTIENT (TIMES A N) P) (QUOT-LIST (SUB1 N) A P))))
(DEFN REM-LIST
(N A P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES A N) P) (REM-LIST (SUB1 N) A P))))
(PROVE-LEMMA REM-QUOT-LIST
NIL
(EQUAL (TIMES A (PLUS-LIST (POSITIVES N)))
(PLUS (TIMES P (PLUS-LIST (QUOT-LIST N A P)))
(PLUS-LIST (REM-LIST N A P)))))
(DEFN EVEN3 (X) (IF (ZEROP X) T (NOT (EVEN3 (SUB1 X)))))
(PROVE-LEMMA EVEN3-PLUS
(REWRITE)
(EQUAL (EVEN3 (PLUS A B)) (EQUAL (EVEN3 A) (EVEN3 B))))
(PROVE-LEMMA EVEN3-DIFF
(REWRITE)
(IMPLIES (LEQ X P)
(EQUAL (EVEN3 (DIFFERENCE P X))
(EQUAL (EVEN3 P) (EVEN3 X)))))
(PROVE-LEMMA EVEN3-TIMES
(REWRITE)
(EQUAL (EVEN3 (TIMES A B))
(OR (EVEN3 A)
(EVEN3 B))))
(PROVE-LEMMA EVEN3-REM
(REWRITE)
(IMPLIES (NOT (EVEN3 P))
(EQUAL (EVEN3 (DIFFERENCE P (REMAINDER X P)))
(NOT (EVEN3 (REMAINDER X P))))))
(PROVE-LEMMA
EVEN3-REM-REFLECT
(REWRITE)
(IMPLIES (NOT (EVEN3 P))
(EQUAL (RES1 N A P)
(IFF (EVEN3 (PLUS-LIST (REM-LIST N A P)))
(EVEN3 (PLUS-LIST (REFLECT-LIST N A P)))))))
(PROVE-LEMMA PERM-PLUS-LIST-1
(REWRITE)
(IMPLIES (MEMBER X M)
(EQUAL (PLUS X (PLUS-LIST (DELETE X M)))
(PLUS-LIST M))))
(PROVE-LEMMA PERM-PLUS-LIST
NIL
(IMPLIES (PERM L M)
(EQUAL (PLUS-LIST L) (PLUS-LIST M))))
(PROVE-LEMMA EVEN3-EVEN NIL (EQUAL (DIVIDES 2 P) (EVEN3 P)))
(PROVE-LEMMA
PLUS-REFLECT-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P A))
(NOT (EVEN3 P)))
(EQUAL (PLUS-LIST (REFLECT-LIST (QUOTIENT P 2) A P))
(PLUS-LIST (POSITIVES (QUOTIENT P 2)))))
((USE (PERM-PLUS-LIST (M (REFLECT-LIST (QUOTIENT P 2) A P))
(L (POSITIVES (QUOTIENT P 2))))
(PIGEON-HOLE-PRINCIPLE (L (REFLECT-LIST (QUOTIENT P 2)
A
P)))
(EVEN3-EVEN)
(ALL-NON-ZEROP-REFLECT-LIST (B (QUOTIENT P 2))))
(DISABLE PRIME)))
(PROVE-LEMMA EQUALS-HAVE-SAME-PARITY
NIL
(IMPLIES (EQUAL X Y) (EQUAL (EVEN3 X) (EVEN3 Y))))
(PROVE-LEMMA
RES1-QUOT-LIST
NIL
(IMPLIES (AND (PRIME P)
(NOT (EVEN3 P))
(NOT (EVEN3 A))
(NOT (DIVIDES P A)))
(EQUAL (RES1 (QUOTIENT P 2) A P)
(EVEN3 (PLUS-LIST (QUOT-LIST (QUOTIENT P 2)
A
P)))))
((USE
(REM-QUOT-LIST (N (QUOTIENT P 2)))
(EQUALS-HAVE-SAME-PARITY
(X (TIMES A (PLUS-LIST (POSITIVES (QUOTIENT P 2)))))
(Y (PLUS (TIMES P
(PLUS-LIST (QUOT-LIST (QUOTIENT P 2) A P)))
(PLUS-LIST (REM-LIST (QUOTIENT P 2) A P))))))
(DISABLE PRIME)))
(DEFN WINS1
(X L)
(IF (NLISTP L)
0
(IF (LESSP (CAR L) X)
(ADD1 (WINS1 X (CDR L)))
(WINS1 X (CDR L)))))
(DEFN WINS
(K L)
(IF (NLISTP K) 0 (PLUS (WINS1 (CAR K) L) (WINS (CDR K) L))))
(DEFN LOSSES1
(X L)
(IF (NLISTP L)
0
(IF (LESSP X (CAR L))
(ADD1 (LOSSES1 X (CDR L)))
(LOSSES1 X (CDR L)))))
(DEFN LOSSES
(K L)
(IF (NLISTP K)
0
(PLUS (LOSSES1 (CAR K) L) (LOSSES (CDR K) L))))
(PROVE-LEMMA WIN-SOME-LOSE-SOME-1
(REWRITE)
(IMPLIES (AND (NOT (MEMBER X L))
(ALL-NON-ZEROP L))
(EQUAL (PLUS (LOSSES1 X L) (WINS1 X L))
(LENGTH L))))
(PROVE-LEMMA WIN-SOME-LOSE-SOME-2
(REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NON-ZEROP L)
(ALL-NON-ZEROP M))
(EQUAL (PLUS (WINS L M) (LOSSES L M))
(TIMES (LENGTH L) (LENGTH M)))))
(PROVE-LEMMA EQUAL-LOSSES-WINS
(REWRITE)
(EQUAL (LOSSES L M) (WINS M L)))
(PROVE-LEMMA
A-WINNER-EVERY-TIME
(REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NON-ZEROP L)
(ALL-NON-ZEROP M))
(EQUAL (PLUS (WINS L M) (WINS M L))
(TIMES (LENGTH L) (LENGTH M))))
((USE (WIN-SOME-LOSE-SOME-2)) (DISABLE WIN-SOME-LOSE-SOME-2)))
(DEFN MULTS
(N P)
(IF (ZEROP N) NIL (CONS (TIMES N P) (MULTS (SUB1 N) P))))
(PROVE-LEMMA LENGTH-MULTS
(REWRITE)
(EQUAL (LENGTH (MULTS N P)) (FIX N)))
(PROVE-LEMMA LEQ-N-WINS1
NIL
(IMPLIES (LESSP (TIMES N P) A)
(LEQ N (WINS1 A (MULTS N P))))
((INDUCT (MULTS N P))))
(PROVE-LEMMA MONOTONE-WINS1
NIL
(IMPLIES (LEQ N M)
(LEQ (WINS1 A (MULTS N P))
(WINS1 A (MULTS M P))))
((INDUCT (MULTS M P))))
(DEFN QUOT-QUOT-INDUCTION
(A B C D)
(IF (ZEROP B)
T
(IF (ZEROP D)
T
(IF (LESSP A D)
T
(IF (LESSP C B)
T
(QUOT-QUOT-INDUCTION (DIFFERENCE A D)
B
(DIFFERENCE C B)
D))))))
(PROVE-LEMMA LEQ-TIMES-QUOT
NIL
(IMPLIES (AND (NOT (ZEROP B))
(LEQ (TIMES A B) (TIMES C D)))
(LEQ (QUOTIENT A D) (QUOTIENT C B)))
((INDUCT (QUOT-QUOT-INDUCTION A B C D))))
(PROVE-LEMMA LEQ-QUOT-TIMES
NIL
(LEQ (QUOTIENT (TIMES (QUOTIENT P 2) Q) P)
(QUOTIENT Q 2))
((USE (LEQ-TIMES-QUOT (A (TIMES (QUOTIENT P 2) Q))
(D P)
(C Q)
(B 2)))
))
(DEFN MONOTONE-QUOT-INDUCTION
(I J P)
(IF (ZEROP P)
T
(IF (LESSP I P)
T
(IF (LESSP J P)
T
(MONOTONE-QUOT-INDUCTION (DIFFERENCE I P)
(DIFFERENCE J P)
P)))))
(PROVE-LEMMA MONOTONE-QUOT
NIL
(IMPLIES (LEQ J I) (LEQ (QUOTIENT J P)
(QUOTIENT I P)))
((INDUCT (MONOTONE-QUOT-INDUCTION I J P))))
(PROVE-LEMMA LEQ-QUOT-TIMES-2
NIL
(IMPLIES (LEQ J (QUOTIENT P 2))
(LEQ (QUOTIENT (TIMES J Q) P)
(QUOTIENT Q 2)))
((USE (LEQ-QUOT-TIMES)
(MONOTONE-QUOT (J (TIMES J Q))
(I (TIMES (QUOTIENT P 2) Q)))
(LESSP-TIMES-CANCELLATION (X J)
(Y (QUOTIENT P 2))
(Z Q)))
(DISABLE LESSP-TIMES-CANCELLATION)))
(PROVE-LEMMA LEQ-QUOT-WINS1-1
NIL
(IMPLIES (NOT (DIVIDES P X))
(LESSP (TIMES (QUOTIENT X P) P) X)))
(PROVE-LEMMA
LEQ-QUOT-WINS1-2
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(NOT (ZEROP Q))
(NOT (ZEROP J))
(LESSP J P))
(LESSP (TIMES (QUOTIENT (TIMES J Q) P) P) (TIMES J Q)))
((USE (LEQ-QUOT-WINS1-1 (X (TIMES J Q)))) (DISABLE PRIME
QUOTIENT
TIMES)))
(PROVE-LEMMA LEQ-QUOT-WINS1
NIL
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(LEQ J (QUOTIENT P 2))
(NOT (ZEROP J))
(NOT (ZEROP Q)))
(LEQ (QUOTIENT (TIMES J Q) P)
(WINS1 (TIMES J Q)
(MULTS (QUOTIENT Q 2) P))))
((USE (LEQ-QUOT-TIMES-2)
(MONOTONE-WINS1 (A (TIMES J Q))
(N (QUOTIENT (TIMES J Q) P))
(M (QUOTIENT Q 2)))
(LEQ-N-WINS1 (A (TIMES J Q))
(N (QUOTIENT (TIMES J Q) P)))
(LEQ-QUOT-WINS1-2))
(DISABLE PRIME)))
(DEFN WINS2
(A N P)
(IF (ZEROP N)
0
(IF (LESSP (TIMES N P) A) N (WINS2 A (SUB1 N) P))))
(PROVE-LEMMA LEQ-WINS2 NIL (LEQ (TIMES (WINS2 A N P) P) A))
(PROVE-LEMMA LEQ-WINS1-N NIL (LEQ (WINS1 A (MULTS N P)) N))
(PROVE-LEMMA LEQ-WINS1-WINS2
NIL
(LEQ (WINS1 A (MULTS N P)) (WINS2 A N P))
((USE (LEQ-WINS1-N)) (INDUCT (WINS2 A N P))))
(PROVE-LEMMA LEQ-WINS1
NIL
(LEQ (TIMES (WINS1 A (MULTS N P)) P) A)
((USE (LEQ-WINS2)
(LEQ-WINS1-WINS2)
(LESSP-TIMES-CANCELLATION (X (WINS1 A
(MULTS N
P)))
(Y (WINS2 A N P))
(Z P)))
(DISABLE LESSP-TIMES-CANCELLATION)))
(PROVE-LEMMA LEQ-WINS1-QUOT
NIL
(IMPLIES (NOT (ZEROP P))
(LEQ (WINS1 A (MULTS N P)) (QUOTIENT A P)))
((USE (MONOTONE-QUOT (I A)
(J (TIMES (WINS1 A (MULTS N P))
P)))
(LEQ-WINS1))
))
(PROVE-LEMMA EQUAL-QUOT-WINS1
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(LEQ J (QUOTIENT P 2))
(NOT (ZEROP J))
(NOT (ZEROP Q)))
(EQUAL (WINS1 (TIMES J Q)
(MULTS (QUOTIENT Q 2) P))
(QUOTIENT (TIMES J Q) P)))
((USE (LEQ-QUOT-WINS1)
(LEQ-WINS1-QUOT (A (TIMES J Q))
(N (QUOTIENT Q 2))))))
(PROVE-LEMMA EQUAL-WINS-PLUS-QUOT-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(NOT (ZEROP Q))
(NOT (ZEROP J))
(LEQ J (QUOTIENT P 2)))
(EQUAL (WINS (MULTS J Q)
(MULTS (QUOTIENT Q 2) P))
(PLUS-LIST (QUOT-LIST J Q P))))
((INDUCT (MULTS J Q))))
(PROVE-LEMMA GAUSS-COROLLARY
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2))
(NOT (EQUAL P Q)))
(EQUAL (RES1 (QUOTIENT P 2) Q P)
(RESIDUE Q P)))
((USE (GAUSS-LEMMA (A Q))) (DISABLE RES1
RESIDUE
QUOTIENT
PRIME1
REMAINDER)))
(PROVE-LEMMA
RESIDUE-QUOT-LIST
NIL
(IMPLIES
(AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2)))
(EQUAL (EQUAL (RESIDUE Q P) (RESIDUE P Q))
(EVEN3 (PLUS (PLUS-LIST (QUOT-LIST (QUOTIENT P 2) Q P))
(PLUS-LIST (QUOT-LIST (QUOTIENT Q 2) P Q))))))
((USE (RES1-QUOT-LIST (A Q))
(RES1-QUOT-LIST (A P) (P Q))
(EVEN3-EVEN)
(EVEN3-EVEN (P Q)))
(DISABLE RESIDUE
RES1
QUOTIENT
QUOT-LIST
PLUS-LIST
LESSP-REMAINDER-DIVISOR
DIFFERENCE
LESSP)))
(PROVE-LEMMA ALL-NON-ZEROP-MULTS
(REWRITE)
(IMPLIES (NOT (ZEROP P)) (ALL-NON-ZEROP (MULTS N P))))
;; (SWAP-OUT "GAUSS-TEMP-LIB-2")
(MAKE-LIB "H-TEMP")
(NOTE-LIB "H-TEMP.LIB" "H-TEMP.LISP")
(PROVE-LEMMA EMPTY-INTERSECT-MULTS-1
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(LESSP I Q)
(LESSP J P))
(NOT (MEMBER (TIMES I P) (MULTS J Q))))
((INDUCT (MULTS J Q))))
(PROVE-LEMMA
EMPTY-INTERSECT-MULTS
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(LESSP I Q))
(NOT (LISTP (INTERSECT (MULTS I P)
(MULTS (QUOTIENT P 2) Q)))))
((USE (EMPTY-INTERSECT-MULTS-1 (J (QUOTIENT P 2))))
(INDUCT (MULTS I P))
(DISABLE PRIME1
QUOTIENT
EMPTY-INTERSECT-MULTS-1
LESSP-REMAINDER-DIVISOR)))
(PROVE-LEMMA
EQUAL-PLUS-QUOT-LIST-WINS
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (PLUS-LIST (QUOT-LIST (QUOTIENT P 2) Q P))
(WINS (MULTS (QUOTIENT P 2) Q)
(MULTS (QUOTIENT Q 2) P))))
((USE (EQUAL-WINS-PLUS-QUOT-LIST (J (QUOTIENT P 2))))
(DISABLE EQUAL-WINS-PLUS-QUOT-LIST
MULTS
QUOT-LIST
WINS
PLUS-LIST
PRIME1)))
(PROVE-LEMMA LAW-OF-QUADRATIC-RECIPROCITY
NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NOT (EQUAL P 2))
(NOT (EQUAL Q 2)))
(EQUAL (EQUAL (RESIDUE Q P) (RESIDUE P Q))
(EVEN (TIMES (QUOTIENT P 2)
(QUOTIENT Q 2)))))
((USE (RESIDUE-QUOT-LIST)
(EVEN3-EVEN (P (TIMES (QUOTIENT P 2)
(QUOTIENT Q 2)))))
(HANDS-OFF QUOTIENT QUOT-LIST EVEN3 RESIDUE TIMES)
(DISABLE RESIDUE
PRIME1
QUOT-LIST
PLUS-LIST
EVEN3-PLUS
LESSP-REMAINDER-DIVISOR))))
NIL "GAUSS")
;;; "FORTRAN"
(PROVEALL
'((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
(DEFN LOGICALP (X)
(OR (EQUAL X (TRUE))
(EQUAL X (FALSE))))
(DEFN EXPT (I J)
(IF (ZEROP J)
1
(TIMES I (EXPT I (SUB1 J)))))
(DEFN ZNUMBERP (X)
(OR (NEGATIVEP X)
(NUMBERP X)))
(DEFN ZZERO NIL (ZERO))
(DEFN ZPLUS (X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(IF (LESSP Y (NEGATIVE-GUTS X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
Y))
(DIFFERENCE Y (NEGATIVE-GUTS X))))
(IF (NEGATIVEP Y)
(IF (LESSP X (NEGATIVE-GUTS Y))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
X))
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(PLUS X Y))))
(DEFN ZDIFFERENCE (X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(IF (LESSP (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(DIFFERENCE (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X)))
(MINUS (PLUS (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(PLUS X (NEGATIVE-GUTS Y))
(IF (LESSP X Y)
(MINUS (DIFFERENCE Y X))
(DIFFERENCE X Y)))))
(DEFN ZTIMES (X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(TIMES (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(MINUS (TIMES (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(MINUS (TIMES X (NEGATIVE-GUTS Y)))
(TIMES X Y))))
(DEFN ZQUOTIENT (X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(QUOTIENT (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
(MINUS (QUOTIENT (NEGATIVE-GUTS X)
Y)))
(IF (NEGATIVEP Y)
(MINUS (QUOTIENT X (NEGATIVE-GUTS Y)))
(QUOTIENT X Y))))
(DEFN ZEXPTZ (I J)
(IF (ZEROP J)
1
(ZTIMES I (ZEXPTZ I (SUB1 J)))))
(DEFN ZNORMALIZE (X)
(IF (NEGATIVEP X)
(IF (EQUAL (NEGATIVE-GUTS X)
0)
0 X)
(FIX X)))
(DEFN ZEQP (X Y)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE Y)))
(DEFN ZNEQP (X Y)
(NOT (ZEQP X Y)))
(DEFN ZLESSP (X Y)
(IF (NEGATIVEP X)
(IF (NEGATIVEP Y)
(LESSP (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS X))
(NOT (AND (EQUAL (NEGATIVE-GUTS X)
0)
(ZEROP Y))))
(IF (NEGATIVEP Y)
F
(LESSP X Y))))
(DEFN ZLESSEQP (X Y)
(NOT (ZLESSP Y X)))
(DEFN ZGREATERP (X Y)
(ZLESSP Y X))
(DEFN ZGREATEREQP (X Y)
(NOT (ZLESSP X Y)))
(DCL GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER NIL) (DCL LEAST-INEXPRESSIBLE-POSITIVE-INTEGER )
(DEFN EXPRESSIBLE-ZNUMBERP (X)
(AND (ZLESSP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)
X)
(ZLESSP X (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))
(DEFN IABS (I)
(IF (NEGATIVEP I)
(NEGATIVE-GUTS I)
(FIX I)))
(DEFN MOD (X Y)
(ZDIFFERENCE X (ZTIMES Y (ZQUOTIENT X Y))))
(DEFN MAX0 (I J)
(IF (ZLESSP I J)
J I))
(DEFN MIN0 (I J)
(IF (ZLESSP I J)
I J))
(DEFN ISIGN (I J)
(IF (NEGATIVEP J)
(ZTIMES -1 (IABS I))
(IABS I)))
(DEFN IDIM (I J)
(ZDIFFERENCE I (MIN0 I J)))
(ADD-SHELL UNDEF NIL UNDEFINED ((UNDEF-GUTS (NONE-OF)
ZERO)))
(DEFN DEFINEDP (X)
(NOT (UNDEFINED X)))
(DCL ELT1 (A I))
(DCL ELT2 (A I J))
(DCL ELT3 (A I J K))
(DEFN LEX (L1 L2)
(IF (OR (NLISTP L1)
(NLISTP L2))
F
(OR (LESSP (CAR L1)
(CAR L2))
(AND (EQUAL (CAR L1)
(CAR L2))
(LEX (CDR L1)
(CDR L2))))))
(DCL RNUMBERP (X))
(DCL DNUMBERP (X))
(DCL CNUMBERP (X))
(DCL RZERO NIL)
(DCL DZERO NIL)
(DCL CZERO NIL)
(DCL EXPRESSIBLE-RNUMBERP (X))
(DCL EXPRESSIBLE-DNUMBERP (X))
(DCL EXPRESSIBLE-CNUMBERP (X))
(DCL RPLUS (X Y))
(DCL RTIMES (X Y))
(DCL RDIFFERENCE (X Y))
(DCL RQUOTIENT (X Y))
(DCL RLESSP (X Y))
(DCL RLESSEQP (X Y))
(DCL REQP (X Y))
(DCL RNEQP (X Y))
(DCL RGREATEREQP (X Y))
(DCL RGREATERP (X Y))
(DCL DPLUS (X Y))
(DCL DTIMES (X Y))
(DCL DDIFFERENCE (X Y))
(DCL DQUOTIENT (X Y))
(DCL DLESSP (X Y))
(DCL DLESSEQP (X Y))
(DCL DEQP (X Y))
(DCL DNEQP (X Y))
(DCL DGREATEREQP (X Y))
(DCL DGREATERP (X Y))
(DCL CPLUS (X Y))
(DCL CTIMES (X Y))
(DCL CDIFFERENCE (X Y))
(DCL CQUOTIENT (X Y))
(DCL CEQP (X Y))
(DCL CNEQP (X Y))
(DCL REXPTZ (X Y))
(DCL DEXPTZ (X Y))
(DCL CEXPTZ (X Y))
(DCL REXPTR (X Y))
(DCL REXPTD (X Y))
(DCL DEXPTR (X Y))
(DCL DEXPTD (X Y))
(DCL ABS (I))
(DCL DABS (I))
(DCL AINT (I))
(DCL INT (I))
(DCL IDINT (I))
(DCL AMOD (I J))
(DCL AMAX0 (I J))
(DCL AMAX1 (I J))
(DCL MAX1 (I J))
(DCL DMAX1 (I J))
(DCL AMIN0 (I J))
(DCL AMIN1 (I J))
(DCL MIN1 (I J))
(DCL DMIN1 (I J))
(DCL FLOAT (I))
(DCL IFIX (I))
(DCL SIGN (I J))
(DCL DSIGN (I J))
(DCL DIM (I J))
(DCL SNGL (I))
(DCL REAL (I))
(DCL AIMAG (I))
(DCL DBLE (I))
(DCL CMPLX (I J))
(DCL CONJG (I))
(DCL EXP (I))
(DCL DEXP (I))
(DCL CEXP (I))
(DCL ALOG (I))
(DCL DLOG (I))
(DCL CLOG (I))
(DCL ALOG10 (I))
(DCL DLOG10 (I))
(DCL SIN (I))
(DCL DSIN (I))
(DCL CSIN (I))
(DCL COS (I))
(DCL DCOS (I))
(DCL CCOS (I))
(DCL TANH (I))
(DCL SQRT (I))
(DCL DSQRT (I))
(DCL CSQRT (I))
(DCL ATAN (I))
(DCL DATAN (I))
(DCL ATAN2 (I J))
(DCL DATAN2 (I J))
(DCL DMOD (I J))
(DCL CABS (I))
(ADD-AXIOM INTEGER-SIZE (REWRITE)
(AND (NUMBERP (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NEGATIVEP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
(LESSP 200 (NEGATIVE-GUTS
(GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)))
(LESSP 200 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))
(DEFN ALMOST-EQUAL1 (A1 A2 U V I E)
(IF (OR (ZEROP V)
(LESSP V U))
T
(AND (IF (EQUAL V I)
(EQUAL (ELT1 A2 V)
E)
(EQUAL (ELT1 A2 V)
(ELT1 A1 V)))
(ALMOST-EQUAL1 A1 A2 U (SUB1 V)
I E))))
(PROVE-LEMMA PLUS-0 (REWRITE)
(EQUAL (PLUS X 0)
(FIX X)))
(PROVE-LEMMA PLUS-NON-NUMBERP (REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (PLUS X Y)
(FIX X))))
(PROVE-LEMMA PLUS-ADD1 (REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X))))
(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE)
(EQUAL (PLUS X (PLUS Y Z))
(PLUS Y (PLUS X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z))))
(PROVE-LEMMA TIMES-0 (REWRITE)
(EQUAL (TIMES X 0)
0))
(PROVE-LEMMA TIMES-NON-NUMBERP (REWRITE)
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X Y)
0)))
(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (REWRITE)
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z))))
(PROVE-LEMMA TIMES-ADD1 (REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X))))
(PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE)
(EQUAL (TIMES X (TIMES Y Z))
(TIMES Y (TIMES X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE)
(EQUAL (TIMES X Y)
(TIMES Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE)
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z))))
(PROVE-LEMMA EQUAL-TIMES-0 (REWRITE)
(EQUAL (EQUAL (TIMES X Y)
0)
(OR (ZEROP X)
(ZEROP Y))))
(PROVE-LEMMA EQUAL-LESSP (REWRITE)
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z))))
(PROVE-LEMMA ALMOST-EQUAL1-IN-RANGE (REWRITE)
(IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
W))
(EQUAL W (IF (EQUAL J I)
E
(ELT1 A1 J)))
(NOT (ZEROP U))
(NOT (LESSP J U))
(NOT (LESSP V J)))
(NOT (ALMOST-EQUAL1 A1 A2 U V I E))))
(PROVE-LEMMA ALMOST-EQUAL1-IN-RANGE-OPENED-UP (REWRITE)
(IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
W))
(EQUAL W (IF (EQUAL J I)
E
(ELT1 A1 J)))
(NOT (ZEROP U))
(LEQ U J)
(LEQ J V)
(NOT (ZEROP V))
(NOT (LESSP V U))
(NOT (EQUAL V I))
(EQUAL (ELT1 A2 V)
(ELT1 A1 V)))
(NOT (ALMOST-EQUAL1 A1 A2 U (SUB1 V)
I E)))
((USE (ALMOST-EQUAL1-IN-RANGE))
(DISABLE ALMOST-EQUAL1-IN-RANGE)))
(PROVE-LEMMA ALMOST-EQUAL1-CONTRACTS (REWRITE)
(IMPLIES (AND (ALMOST-EQUAL1 A1 A2 U V I E)
(NOT (ZEROP U))
(NOT (LESSP X U))
(NOT (LESSP V Y)))
(ALMOST-EQUAL1 A1 A2 X Y I E))
NIL))
NIL "FORTRAN")
;;; "CONTROLLER"
(PROVEALL
'((NOTE-LIB "FORTRAN.LIB" "FORTRAN.LISP")
(PROVE-LEMMA ZPLUS-COMM1 (REWRITE)
(EQUAL (ZPLUS X Y)
(ZPLUS Y X)))
(PROVE-LEMMA ZPLUS-COMM2 (REWRITE)
(EQUAL (ZPLUS X (ZPLUS Y Z))
(ZPLUS Y (ZPLUS X Z))))
(PROVE-LEMMA ZPLUS-ASSOC (REWRITE)
(EQUAL (ZPLUS (ZPLUS X Y)
Z)
(ZPLUS X (ZPLUS Y Z))))
(DISABLE ZPLUS)
(ADD-SHELL VEHICLE-STATE NIL VEHICLE-STATEP ((W (NONE-OF)
ZERO)
(Y (NONE-OF)
ZERO)
(V (NONE-OF)
ZERO)))
(DEFN HD (X)
(CAR X))
(DEFN TL (X)
(CDR X))
(DEFN EMPTY (X)
(NOT (LISTP X)))
(PROVE-LEMMA TL-REWRITE (REWRITE)
(EQUAL (TL X)
(CDR X)))
(DISABLE TL)
(PROVE-LEMMA DOWN-ON-TL (REWRITE)
(IMPLIES (NOT (EMPTY X))
(LESSP (COUNT (TL X))
(COUNT X))))
(DEFN RANDOM-DELTA-WS (LST)
(IF (EMPTY LST)
T
(AND (OR (EQUAL (HD LST)
-1)
(EQUAL (HD LST)
0)
(EQUAL (HD LST)
1))
(RANDOM-DELTA-WS (TL LST)))))
(DEFN CONTROLLER (SGN-Y SGN-OLD-Y)
(ZPLUS (ZTIMES -3 SGN-Y)
(ZTIMES 2 SGN-OLD-Y)))
(DISABLE CONTROLLER)
(DEFN SGN (X)
(IF (NEGATIVEP X)
(IF (EQUAL (NEGATIVE-GUTS X)
0)
0 -1)
(IF (ZEROP X)
0 1)))
(DISABLE SGN)
(DEFN
NEXT-STATE
(DELTA-W STATE)
(VEHICLE-STATE
(ZPLUS (W STATE)
DELTA-W)
(ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE)
DELTA-W)))
(ZPLUS (V STATE)
(CONTROLLER (SGN (ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE)
DELTA-W))))
(SGN (Y STATE))))))
(DEFN FINAL-STATE-OF-VEHICLE (DELTA-WS STATE)
(IF (EMPTY DELTA-WS)
STATE
(FINAL-STATE-OF-VEHICLE (TL DELTA-WS)
(NEXT-STATE (HD DELTA-WS)
STATE))))
(DEFN
GOOD-STATEP
(STATE)
(IF
(EQUAL (Y STATE)
0)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
0)
(EQUAL (ZPLUS (V STATE)
(W STATE))
1))
(IF
(EQUAL (Y STATE)
1)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-2)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-3))
(IF
(EQUAL (Y STATE)
2)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-2))
(IF (EQUAL (Y STATE)
3)
(EQUAL (ZPLUS (V STATE)
(W STATE))
-1)
(IF (EQUAL (Y STATE)
-3)
(EQUAL (ZPLUS (V STATE)
(W STATE))
1)
(IF (EQUAL (Y STATE)
-2)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
1)
(EQUAL (ZPLUS (V STATE)
(W STATE))
2))
(IF (EQUAL (Y STATE)
-1)
(OR (EQUAL (ZPLUS (V STATE)
(W STATE))
2)
(EQUAL (ZPLUS (V STATE)
(W STATE))
3))
F))))))))
(PROVE-LEMMA NEXT-GOOD-STATE (REWRITE)
(IMPLIES (AND (GOOD-STATEP STATE)
(OR (EQUAL R -1)
(EQUAL R 0)
(EQUAL R 1)))
(GOOD-STATEP (NEXT-STATE R STATE))))
(DEFN ZERO-DELTA-WS (LST)
(IF (EMPTY LST)
T
(AND (EQUAL (HD LST)
0)
(ZERO-DELTA-WS (TL LST)))))
(DEFN APPEND (X Y)
(IF (EMPTY X)
Y
(CONS (HD X)
(APPEND (TL X)
Y))))
(PROVE-LEMMA LENGTH-0 (REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(EMPTY X)))
(PROVE-LEMMA
DECOMPOSE-LIST-OF-LENGTH-4
(REWRITE)
(IMPLIES (ZERO-DELTA-WS LST)
(EQUAL (LESSP (LENGTH LST)
4)
(NOT (EQUAL LST (APPEND (QUOTE (0 0 0 0))
(CDDDDR LST)))))))
(PROVE-LEMMA DRIFT-TO-0-IN-4 (REWRITE)
(IMPLIES
(GOOD-STATEP STATE)
(EQUAL (Y (FINAL-STATE-OF-VEHICLE
(QUOTE (0 0 0 0))
STATE))
0)))
(PROVE-LEMMA
CANCEL-WIND-IN-4
(REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE
(QUOTE (0 0 0 0))
STATE))
(W (FINAL-STATE-OF-VEHICLE
(QUOTE (0 0 0 0))
STATE)))
0)))
(PROVE-LEMMA
ONCE-0-ALWAYS-0
(REWRITE)
(IMPLIES
(AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE)
0)
(EQUAL (ZPLUS (W STATE)
(V STATE))
0))
(AND (EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0))))
(PROVE-LEMMA FINAL-STATE-OF-VEHICLE-APPEND (REWRITE)
(EQUAL (FINAL-STATE-OF-VEHICLE (APPEND A B)
STATE)
(FINAL-STATE-OF-VEHICLE
B
(FINAL-STATE-OF-VEHICLE A STATE))))
(PROVE-LEMMA ZERO-DELTA-WS-APPEND (REWRITE)
(EQUAL (ZERO-DELTA-WS (APPEND (QUOTE (0 0 0 0))
V))
(ZERO-DELTA-WS V)))
(DISABLE APPEND)
(DISABLE NEXT-STATE)
(PROVE-LEMMA GOOD-STATEP-BOUNDED-ABOVE (REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP 3 (Y STATE)))))
(PROVE-LEMMA GOOD-STATEP-BOUNDED-BELOW (REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP (Y STATE)
-3))))
(DISABLE GOOD-STATEP)
(PROVE-LEMMA ZLESSP-IS-LESSP (REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y))
(EQUAL (ZLESSP X Y)
(LESSP X Y))))
(DISABLE ZLESSP)
(DEFN FSV (D S)
(IF (EMPTY D)
S
(FSV (TL D)
(NEXT-STATE (HD D)
S))))
(PROVE-LEMMA ALL-GOOD-STATES (REWRITE)
(IMPLIES (AND (RANDOM-DELTA-WS LST)
(GOOD-STATEP STATE))
(GOOD-STATEP
(FINAL-STATE-OF-VEHICLE LST STATE)))
((INDUCT (FSV LST STATE))))
(PROVE-LEMMA VEHICLE-STAYS-WITHIN-3-OF-COURSE NIL
(IMPLIES
(AND (RANDOM-DELTA-WS LST)
(EQUAL STATE (FINAL-STATE-OF-VEHICLE
LST
(VEHICLE-STATE 0 0 0))))
(AND (ZLESSEQP -3 (Y STATE))
(ZLESSEQP (Y STATE)
3))))
(DISABLE FINAL-STATE-OF-VEHICLE)
(PROVE-LEMMA ZERO-DELTA-WS-CDDDDR (REWRITE)
(IMPLIES (ZERO-DELTA-WS X)
(ZERO-DELTA-WS (CDDDDR X))))
(PROVE-LEMMA GOOD-STATES-FIND-AND-STAY-AT-0 (REWRITE)
(IMPLIES
(AND (GOOD-STATEP STATE)
(ZERO-DELTA-WS LST2)
(NOT (LESSP (LENGTH LST2)
4)))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST2 STATE))
0)))
(PROVE-LEMMA VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND NIL
(IMPLIES
(AND (RANDOM-DELTA-WS LST1)
(ZERO-DELTA-WS LST2)
(ZGREATEREQP (LENGTH LST2)
4)
(EQUAL STATE (FINAL-STATE-OF-VEHICLE
(APPEND LST1 LST2)
(VEHICLE-STATE 0 0 0))))
(EQUAL (Y STATE)
0))
NIL))
NIL "CONTROLLER")
;;; "PR"
(PROVEALL
'((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
; The floor of the square root. This definition is taken from Goodstein.
(DEFN RT (X)
(IF (ZEROP X)
0
(IF (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(ADD1 (RT (SUB1 X)))
(RT (SUB1 X)))))
(PROVE-LEMMA TIMES-ADD1 (REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(PLUS X (TIMES X Y))))
(PROVE-LEMMA PLUS-ADD1 (REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(ADD1 (PLUS X Y))))
(PROVE-LEMMA SQUARE-0 (REWRITE)
(EQUAL (EQUAL (TIMES X X)
0)
(ZEROP X)))
(PROVE-LEMMA SQUARE-MONOTONIC NIL
(IMPLIES (NOT (LESSP B A))
(NOT (LESSP (TIMES B B)
(TIMES A A)))))
(PROVE-LEMMA
SPEC-FOR-RT NIL
(AND (NOT (LESSP Y (TIMES (RT Y)
(RT Y))))
(LESSP Y (ADD1 (PLUS (RT Y)
(PLUS (RT Y)
(TIMES (RT Y)
(RT Y))))))))
(PROVE-LEMMA RT-IS-UNIQUE NIL
(IMPLIES (AND (NUMBERP A)
(LEQ (TIMES A A)
Y)
(LESSP Y (TIMES (ADD1 A)
(ADD1 A))))
(EQUAL A (RT Y)))
((USE (SPEC-FOR-RT)
(SQUARE-MONOTONIC (A (ADD1 A))
(B (RT Y)))
(SQUARE-MONOTONIC (A (ADD1 (RT Y)))
(B A)))))
(PROVE-LEMMA NCONS-LEMMA (REWRITE)
(EQUAL (RT (PLUS U (TIMES (PLUS U V)
(PLUS U V))))
(PLUS U V))
((USE (RT-IS-UNIQUE
(Y (PLUS U (TIMES (PLUS U V)
(PLUS U V))))
(A (PLUS U V))))))
(DEFN NCAR (X)
(DIFFERENCE X (TIMES (RT X)
(RT X))))
(DEFN NCDR (X)
(DIFFERENCE (RT X)
(NCAR X)))
(DEFN NCONS (I J)
(PLUS I (TIMES (PLUS I J)
(PLUS I J))))
(PROVE-LEMMA NCAR-NCONS NIL (IMPLIES (NUMBERP I)
(EQUAL (NCAR (NCONS I J))
I)))
(PROVE-LEMMA NCDR-NCONS NIL (IMPLIES (NUMBERP J)
(EQUAL (NCDR (NCONS I J))
J)))
(DEFN NCADR (X)
(NCAR (NCDR X)))
(DEFN NCADDR (X)
(NCAR (NCDR (NCDR X))))
(PROVE-LEMMA RT-LESSP (REWRITE)
(IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL X 1)))
(LESSP (RT X)
X)))
; I'm sure the system could prove this without the hint, but it would use
; induction and this is the obvious way to do it.
(PROVE-LEMMA RT-LESSEQP (REWRITE)
(NOT (LESSP X (RT X)))
((USE (RT-LESSP))))
(PROVE-LEMMA DIFFERENCE-0 (REWRITE)
(IMPLIES (LESSP X Y)
(EQUAL (DIFFERENCE X Y)
0)))
(PROVE-LEMMA LESSP-DIFFERENCE-1 (REWRITE)
(EQUAL (LESSP (DIFFERENCE A B)
C)
(IF (LESSP A B)
(LESSP 0 C)
(LESSP A (PLUS B C)))))
(PROVE-LEMMA NCAR-LESSEQP (REWRITE)
(NOT (LESSP X (NCAR X))))
(PROVE-LEMMA CROCK (REWRITE)
(EQUAL (LESSP X (DIFFERENCE (RT X)
D))
F)
NIL
; This disgusting fact is needed because linear seems to have trouble with
; nests of DIFFERENCEs. Try disabling this and proving NCDR-LESSEQP below and
; observe that when D is a DIFFERENCE expression we don't prove it.
)
(PROVE-LEMMA NCDR-LESSEQP (REWRITE)
(NOT (LESSP X (NCDR X))))
(PROVE-LEMMA NCDR-LESSP (REWRITE)
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (NCAR FN)
0))
(NOT (EQUAL (NCAR FN)
1)))
(LESSP (NCDR FN)
FN)))
(DISABLE NCAR)
(DISABLE NCDR)
(DEFN
PR-APPLY
(FN ARG)
(IF
(NOT (NUMBERP FN))
0
(IF
(EQUAL (NCAR FN)
0)
0
(IF
(EQUAL (NCAR FN)
1)
ARG
(IF
(EQUAL (NCAR FN)
2)
(ADD1 ARG)
(IF
(EQUAL (NCAR FN)
3)
(RT ARG)
(IF
(EQUAL (NCAR FN)
4)
(IF (ZEROP ARG)
0
(PR-APPLY (NCDR FN)
(PR-APPLY FN (SUB1 ARG))))
(IF
(EQUAL (NCAR FN)
5)
(PLUS (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF
(EQUAL (NCAR FN)
6)
(DIFFERENCE (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF (EQUAL (NCAR FN)
7)
(TIMES (PR-APPLY (NCADR FN)
ARG)
(PR-APPLY (NCADDR FN)
ARG))
(IF (EQUAL (NCAR FN)
8)
(PR-APPLY (NCADR FN)
(PR-APPLY (NCADDR FN)
ARG))
0))))))))))
((LEX2 (LIST (COUNT FN)
(COUNT ARG)))))
(DEFN NON-PR-FN (X)
(ADD1 (PR-APPLY X X)))
(DEFN COUNTER-EXAMPLE-FOR (X)
(FIX X))
(PROVE-LEMMA NON-PR-FUNCTIONS-EXIST NIL
(NOT (EQUAL (NON-PR-FN (COUNTER-EXAMPLE-FOR FN))
(PR-APPLY FN
(COUNTER-EXAMPLE-FOR FN)))))
(PROVE-LEMMA COUNTER-EXAMPLE-FOR-NUMERIC (REWRITE)
(NUMBERP (COUNTER-EXAMPLE-FOR X)))
(DISABLE PR-APPLY
; Not known to be necessary.
)
(DEFN MAX (I J)
(IF (LESSP I J)
J I))
(DEFN MAX2 (FN I)
(IF (ZEROP I)
(PR-APPLY FN I)
(MAX (PR-APPLY FN I)
(MAX2 FN (SUB1 I)))))
(DEFN MAX1 (FN I)
(IF (ZEROP FN)
(MAX2 FN I)
(MAX (MAX2 FN I)
(MAX1 (SUB1 FN)
I))))
(PROVE-LEMMA MAX2-GTE (REWRITE)
(NOT (LESSP (MAX2 I J)
(PR-APPLY I J))))
(DEFN EXCEED (J)
(ADD1 (MAX1 J J)))
(DEFN EXCEED-AT (I)
I)
(PROVE-LEMMA MAX1-GTE1 (REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN)
I)
(PR-APPLY FN I)))))
(PROVE-LEMMA MAX1-GTE2 (REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN)
(PLUS J FN))
(PR-APPLY FN (PLUS J FN))))))
(PROVE-LEMMA EXCEED-IS-BIGGER NIL
(IMPLIES (NUMBERP FN)
(LESSP (PR-APPLY FN
(PLUS J
(EXCEED-AT FN)))
(EXCEED (PLUS J (EXCEED-AT FN))))))
)
NIL "PR")
;;; "UNSOLV"
(PROVEALL
'((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP") (ADD-SHELL BTM NIL BTMP )
(DEFN GET (X ALIST)
(IF (NLISTP ALIST)
(BTM)
(IF (EQUAL X (CAAR ALIST))
(CDAR ALIST)
(GET X (CDR ALIST)))))
(DEFN PAIRLIST (X Y)
(IF (NLISTP X)
NIL
(CONS (CONS (CAR X)
(CAR Y))
(PAIRLIST (CDR X)
(CDR Y)))))
(DEFN SUBRP (FN)
(MEMBER FN
(QUOTE (ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS
CAR CDR LISTP PACK UNPACK LITATOM
EQUAL LIST))))
(DEFN
APPLY-SUBR
(FN LST)
(IF
(EQUAL FN (QUOTE ZERO))
(ZERO)
(IF
(EQUAL FN (QUOTE TRUE))
(TRUE)
(IF
(EQUAL FN (QUOTE FALSE))
(FALSE)
(IF
(EQUAL FN (QUOTE ADD1))
(ADD1 (CAR LST))
(IF
(EQUAL FN (QUOTE SUB1))
(SUB1 (CAR LST))
(IF
(EQUAL FN (QUOTE NUMBERP))
(NUMBERP (CAR LST))
(IF
(EQUAL FN (QUOTE CONS))
(CONS (CAR LST)
(CADR LST))
(IF
(EQUAL FN (QUOTE LIST))
LST
(IF
(EQUAL FN (QUOTE CAR))
(CAR (CAR LST))
(IF
(EQUAL FN (QUOTE CDR))
(CDR (CAR LST))
(IF
(EQUAL FN (QUOTE LISTP))
(LISTP (CAR LST))
(IF (EQUAL FN (QUOTE PACK))
(PACK (CAR LST))
(IF (EQUAL FN (QUOTE UNPACK))
(UNPACK (CAR LST))
(IF (EQUAL FN (QUOTE LITATOM))
(LITATOM (CAR LST))
(IF (EQUAL FN (QUOTE EQUAL))
(EQUAL (CAR LST)
(CADR LST))
0))))))))))))))))
(DEFN
EV
(FLG X VA FA N)
(IF
(EQUAL FLG (QUOTE AL))
(IF
(NLISTP X)
(IF (NUMBERP X)
X
(IF (EQUAL X (QUOTE T))
T
(IF (EQUAL X (QUOTE F))
F
(IF (EQUAL X NIL)
NIL
(GET X VA)))))
(IF
(EQUAL (CAR X)
(QUOTE QUOTE))
(CADR X)
(IF
(EQUAL (CAR X)
(QUOTE IF))
(IF (BTMP (EV (QUOTE AL)
(CADR X)
VA FA N))
(BTM)
(IF (EV (QUOTE AL)
(CADR X)
VA FA N)
(EV (QUOTE AL)
(CADDR X)
VA FA N)
(EV (QUOTE AL)
(CADDDR X)
VA FA N)))
(IF
(BTMP (EV (QUOTE LIST)
(CDR X)
VA FA N))
(BTM)
(IF
(SUBRP (CAR X))
(APPLY-SUBR (CAR X)
(EV (QUOTE LIST)
(CDR X)
VA FA N))
(IF (BTMP (GET (CAR X)
FA))
(BTM)
(IF (ZEROP N)
(BTM)
(EV (QUOTE AL)
(CADR (GET (CAR X)
FA))
(PAIRLIST (CAR (GET (CAR X)
FA))
(EV (QUOTE LIST)
(CDR X)
VA FA N))
FA
(SUB1 N)))))))))
(IF (LISTP X)
(IF (BTMP (EV (QUOTE AL)
(CAR X)
VA FA N))
(BTM)
(IF (BTMP (EV (QUOTE LIST)
(CDR X)
VA FA N))
(BTM)
(CONS (EV (QUOTE AL)
(CAR X)
VA FA N)
(EV (QUOTE LIST)
(CDR X)
VA FA N))))
NIL))
((LEX2 (LIST N (COUNT X)))))
(DEFN EVAL (X VA FA N)
(EV (QUOTE AL)
X VA FA N))
(DEFN EVLIST (X VA FA N)
(EV (QUOTE LIST)
X VA FA N))
; We now define the functions x, va, fa, and k. To do so we first define
; SUBLIS, which applies a substitution to an s-expression. Then we use the
; names CIRC and LOOP in the definitions of x and fa and use SUBLIS to
; replace those names with "new" names. It is not important whether we have
; defined this notion of substitution correctly, since all that is required
; is that we exhibit some x, va, fa, and k with the desired properties.
(DEFN APPEND (X Y)
(IF (NLISTP X)
Y
(CONS (CAR X)
(APPEND (CDR X)
Y))))
(DEFN ASSOC (VAR ALIST)
(IF (NLISTP ALIST)
F
(IF (EQUAL VAR (CAAR ALIST))
(CAR ALIST)
(ASSOC VAR (CDR ALIST)))))
(DEFN SUBLIS (ALIST X)
(IF (NLISTP X)
(IF (ASSOC X ALIST)
(CDR (ASSOC X ALIST))
X)
(CONS (SUBLIS ALIST (CAR X))
(SUBLIS ALIST (CDR X)))))
(DEFN x (FA)
(SUBLIS (LIST (CONS (QUOTE CIRC)
(CONS FA 0)))
(QUOTE (CIRC A))))
(DEFN
fa
(FA)
(APPEND
(SUBLIS
(LIST (CONS (QUOTE CIRC)
(CONS FA 0))
(CONS (QUOTE LOOP)
(CONS FA 1)))
(QUOTE ((CIRC (A)
(IF (HALTS (QUOTE (CIRC A))
(LIST (CONS (QUOTE A)
A))
A)
(LOOP)
T))
(LOOP NIL (LOOP)))))
FA))
(DEFN va (FA)
(LIST (CONS (QUOTE A)
(fa FA))))
(DEFN k (N)
(ADD1 N))
; We wish to prove that having "new" program names in the function
; environment does not effect the computation of the body of HALTS. To state
; this we must first define formally what we mean by "new". Then we will
; prove the general result we need and then we will instantiate it for the
; particular "new" program names we choose.
(DEFN OCCUR (X Y)
(IF (EQUAL X Y)
T
(IF (NLISTP Y)
F
(OR (OCCUR X (CAR Y))
(OCCUR X (CDR Y))))))
(DEFN OCCUR-IN-DEFNS (X LST)
(IF (NLISTP LST)
F
(OR (OCCUR X (CADDR (CAR LST)))
(OCCUR-IN-DEFNS X (CDR LST))))
NIL
; This function returns T or F according to whether X occurs in the body of
; some defn in LST. At first we avoided using this function and just asked
; instead whether X occurs in LST. However, when so put the following lemma
; is not valid.
)
(PROVE-LEMMA OCCUR-OCCUR-IN-DEFNS (REWRITE)
(IMPLIES (AND (NOT (OCCUR-IN-DEFNS FN FA))
(NOT (BTMP (GET X FA))))
(NOT (OCCUR FN (CADR (GET X FA))))))
(PROVE-LEMMA LEMMA1 (REWRITE)
(IMPLIES (AND (NOT (OCCUR FN X))
(NOT (OCCUR-IN-DEFNS FN FA)))
(EQUAL (EV FLG X VA (CONS (CONS FN DEF)
FA)
N)
(EV FLG X VA FA N)))
NIL
; If a FN is not used in X or any defn in FA then it can be ignored.
)
(PROVE-LEMMA COUNT-OCCUR (REWRITE)
(IMPLIES (LESSP (COUNT Y)
(COUNT X))
(NOT (OCCUR X Y)))
NIL
; This lemma will let us show that the name (CONS FA i) does not occur in FA.
)
(PROVE-LEMMA COUNT-GET (REWRITE)
(LESSP (COUNT (CADR (GET FN FA)))
(ADD1 (COUNT FA)))
NIL
; This lemma will let us show that the name (CONS FA i) does not occur in any
; defn obtained from FA.
)
(PROVE-LEMMA COUNT-OCCUR-IN-DEFNS (REWRITE)
(IMPLIES (LESSP (COUNT FA)
(COUNT X))
(NOT (OCCUR-IN-DEFNS X FA)))
NIL
; This lemma lets us establish that (CONS FA i) doesn't occur in the defns of
; FA.
)
(PROVE-LEMMA
COROLLARY1
(REWRITE)
(EQUAL (EV (QUOTE AL)
(CADR (GET (QUOTE HALTS)
FA))
VA
(CONS (CONS (CONS FA 0)
DEF0)
(CONS (LIST (CONS FA 1)
NIL
(LIST (CONS FA 1)))
FA))
N)
(EV (QUOTE AL)
(CADR (GET (QUOTE HALTS)
FA))
VA FA N))
NIL
; This is the result we needed: evaluating the body of HALTS in an
; environment containing the two new programs CIRC and LOOP produces the same
; result as without those two programs.
)
(DISABLE LEMMA1
; We now turn off the key lemma and just rely on the result just proved.
; Failure to turn off the key lemma causes the system to spend hundred of
; thousands of conses investigating OCCURrences and comparing COUNTs on
; almost every EVAL expression involved in the proof.
)
(PROVE-LEMMA LEMMA2 NIL
(IMPLIES (AND (NOT (BTMP (EV FLG X VA FA N)))
(NOT (BTMP (EV FLG X VA FA K))))
(EQUAL (EV FLG X VA FA N)
(EV FLG X VA FA K)))
NIL
; If EV at N and K are both not BTM then they are equal. We will need only
; COROLLARY2 below, but we must prove the more general version by induction.
)
(PROVE-LEMMA COROLLARY2 (REWRITE)
(IMPLIES (EQUAL (EV FLG X VA FA N)
T)
(EV FLG X VA FA K))
((USE (LEMMA2)))
; If EV at N is T then EV at K is not F. We have to tell the system to use
; LEMMA2 to prove this.
)
(PROVE-LEMMA LEMMA3 (REWRITE)
(IMPLIES (AND (LISTP X)
(LISTP (CAR X))
(NLISTP (CDR X))
(LISTP (GET (CAR X)
FA))
(EQUAL (CAR (GET (CAR X)
FA))
NIL)
(EQUAL (CADR (GET (CAR X)
FA))
X))
(BTMP (EV (QUOTE AL)
X VA FA N)))
; If a program is defined so as to call itself immediately then it never
; terminates.
)
(PROVE-LEMMA
EXPAND-CIRC
(REWRITE)
(IMPLIES
(AND (NOT (BTMP VAL))
(NOT (BTMP (GET (CONS FN 0)
FA))))
(EQUAL
(EV (QUOTE AL)
(CONS (CONS FN 0)
(QUOTE (A)))
(LIST (CONS (QUOTE A)
VAL))
FA J)
(IF (ZEROP J)
(BTM)
(EV (QUOTE AL)
(CADR (GET (CONS FN 0)
FA))
(PAIRLIST (CAR (GET (CONS FN 0)
FA))
(EV (QUOTE LIST)
(QUOTE (A))
(LIST (CONS (QUOTE A)
VAL))
FA J))
FA
(SUB1 J)))))
NIL
; This lemma forces the system to expand any call of EVAL on CIRC. Were CIRC
; defined recursively on the function alist this lemma would cause infinite
; rewriting. Without this lemma the system does not expand the call of EVAL
; on CIRC because it introduces "worse" calls of EVAL, namely on the args of
; the call and body of CIRC. However, once it has stepped from the call of
; CIRC to its body it then the calls.
)
(PROVE-LEMMA UNSOLVABILITY-OF-THE-HALTING-PROBLEM NIL
(IMPLIES (EQUAL H (EVAL (LIST (QUOTE HALTS)
(LIST (QUOTE QUOTE)
(x FA))
(LIST (QUOTE QUOTE)
(va FA))
(LIST (QUOTE QUOTE)
(fa FA)))
NIL FA N))
(AND (IMPLIES (EQUAL H F)
(NOT (BTMP (EVAL (x FA)
(va FA)
(fa FA)
(k N)))))
(IMPLIES (EQUAL H T)
(BTMP (EVAL (x FA)
(va FA)
(fa FA)
K)))))
NIL))
NIL "UNSOLV")
;;; "TMI"
(PROVEALL
'((NOTE-LIB "UNSOLV.LIB" "UNSOLV.LISP")
(DEFN SYMBOL (X)
(MEMBER X (QUOTE (0 1))))
(DEFN HALF-TAPE (X)
(IF (NLISTP X)
(EQUAL X 0)
(AND (SYMBOL (CAR X))
(HALF-TAPE (CDR X)))))
(DEFN TAPE (X)
(AND (LISTP X)
(HALF-TAPE (CAR X))
(HALF-TAPE (CDR X))))
(DEFN OPERATION (X)
(MEMBER X (QUOTE (L R 0 1))))
(DEFN STATE (X)
(LITATOM X))
(DEFN TURING-4TUPLE (X)
(AND (LISTP X)
(STATE (CAR X))
(SYMBOL (CADR X))
(OPERATION (CADDR X))
(STATE (CADDDR X))
(EQUAL (CDDDDR X)
NIL)))
(DEFN TURING-MACHINE (X)
(IF (NLISTP X)
(EQUAL X NIL)
(AND (TURING-4TUPLE (CAR X))
(TURING-MACHINE (CDR X)))))
(DEFN INSTR (ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
(DEFN NEW-TAPE (OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE))
(CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE))
(CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
(DEFN TMI (ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (INSTR ST (CAR (CDR TAPE))
TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE)
TM
(SUB1 N))
TAPE)))
(DEFN INSTR-DEFN NIL
(QUOTE ((ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))))
(DEFN NEW-TAPE-DEFN NIL (QUOTE ((OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE))
(CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE))
(CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP
(CDR (CDR TAPE)))))))))
(DEFN TMI-DEFN NIL (QUOTE ((ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE))
TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM)))
(NEW-TAPE
(CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE)
TM)
TAPE))))
(DEFN KWOTE (X)
(LIST 'QUOTE X))
(DEFN tmi-fa (TM)
(LIST (LIST 'TM NIL (KWOTE TM))
(CONS 'INSTR (INSTR-DEFN))
(CONS 'NEW-TAPE (NEW-TAPE-DEFN))
(CONS 'TMI (TMI-DEFN))))
(DEFN tmi-x (ST TAPE)
(LIST 'TMI (KWOTE ST)
(KWOTE TAPE)
(QUOTE (TM))))
(DEFN tmi-k (ST TAPE TM N)
(DIFFERENCE N (ADD1 (LENGTH TM))))
(DEFN tmi-n (ST TAPE TM K)
(PLUS K (ADD1 (LENGTH TM))))
(PROVE-LEMMA LENGTH-0 (REWRITE)
(EQUAL (EQUAL (LENGTH X)
0)
(NLISTP X)))
(PROVE-LEMMA PLUS-EQUAL-0 (REWRITE)
(EQUAL (EQUAL (PLUS I J)
0)
(AND (ZEROP I)
(ZEROP J))))
(PROVE-LEMMA PLUS-DIFFERENCE (REWRITE)
(EQUAL (PLUS (DIFFERENCE I J)
J)
(IF (LEQ I J)
(FIX J)
I)))
(TOGGLE DIFFERENCE-OFF DIFFERENCE T)
(PROVE-LEMMA EVAL-FN-0 (REWRITE)
(IMPLIES (AND (ZEROP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (SUBRP FN))
(EQUAL VARGS (EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS)
VA FA N)
(BTM))))
(PROVE-LEMMA EVAL-FN-1 (REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (SUBRP FN))
(EQUAL VARGS (EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS)
VA FA N)
(IF (BTMP VARGS)
(BTM)
(IF (BTMP (GET FN FA))
(BTM)
(EV 'AL (CADR (GET FN FA))
(PAIRLIST (CAR (GET FN FA))
VARGS)
FA
(SUB1 N)))))))
(PROVE-LEMMA EVAL-SUBRP (REWRITE)
(IMPLIES (AND (SUBRP FN)
(EQUAL VARGS (EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS)
VA FA N)
(IF (BTMP VARGS)
(BTM)
(APPLY-SUBR FN VARGS)))))
(PROVE-LEMMA EVAL-IF (REWRITE)
(IMPLIES (EQUAL VX1 (EV 'AL X1 VA FA N))
(EQUAL (EV 'AL (LIST 'IF X1 X2 X3)
VA FA N)
(IF (BTMP VX1)
(BTM)
(IF VX1 (EV 'AL X2 VA FA N)
(EV 'AL X3 VA FA N))))))
(PROVE-LEMMA EVAL-QUOTE (REWRITE)
(EQUAL (EV 'AL (LIST 'QUOTE X)
VA FA N)
X))
(PROVE-LEMMA EVAL-NLISTP (REWRITE)
(AND (EQUAL (EV 'AL 0 VA FA N)
0)
(EQUAL (EV 'AL (ADD1 N)
VA FA N)
(ADD1 N))
(EQUAL (EV 'AL (PACK X)
VA FA N)
(IF (EQUAL (PACK X)
(QUOTE T))
T
(IF (EQUAL (PACK X)
'F)
F
(IF (EQUAL (PACK X)
(QUOTE NIL))
NIL
(GET (PACK X)
VA)))))))
(PROVE-LEMMA EVLIST-NIL (REWRITE)
(EQUAL (EV 'LIST NIL VA FA N)
NIL))
(PROVE-LEMMA EVLIST-CONS (REWRITE)
(IMPLIES (AND (EQUAL VX (EV 'AL X VA FA N))
(EQUAL VL (EV 'LIST L VA FA N)))
(EQUAL (EV 'LIST (CONS X L)
VA FA N)
(IF (BTMP VX)
(BTM)
(IF (BTMP VL)
(BTM)
(CONS VX VL))))))
(TOGGLE SUBRP-OFF SUBRP T)
(TOGGLE EV-OFF EV T)
(DEFN CNB (X)
(IF (LISTP X)
(AND (CNB (CAR X))
(CNB (CDR X)))
(NOT (BTMP X))))
(PROVE-LEMMA CNB-NBTM (REWRITE)
(IMPLIES (CNB X)
(NOT (BTMP X))))
(PROVE-LEMMA CNB-CONS (REWRITE)
(AND (EQUAL (CNB (CONS A B))
(AND (CNB A)
(CNB B)))
(IMPLIES (CNB X)
(CNB (CAR X)))
(IMPLIES (CNB X)
(CNB (CDR X)))))
(PROVE-LEMMA CNB-LITATOM (REWRITE)
(IMPLIES (LITATOM X)
(CNB X)))
(PROVE-LEMMA CNB-NUMBERP (REWRITE)
(IMPLIES (NUMBERP X)
(CNB X)))
(TOGGLE CNB-OFF CNB T)
(PROVE-LEMMA GET-tmi-fa (REWRITE)
(AND (EQUAL (GET 'TM (tmi-fa TM))
(LIST NIL (KWOTE TM)))
(EQUAL (GET 'INSTR (tmi-fa TM))
(INSTR-DEFN))
(EQUAL (GET 'NEW-TAPE (tmi-fa TM))
(NEW-TAPE-DEFN))
(EQUAL (GET 'TMI (tmi-fa TM))
(TMI-DEFN))))
(TOGGLE tmi-fa-OFF tmi-fa T)
(DEFN INSTRN (ST SYM TM N)
(IF (ZEROP N)
(BTM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTRN ST SYM (CDR TM)
(SUB1 N)))
(INSTRN ST SYM (CDR TM)
(SUB1 N)))
F)))
(DEFN EVAL-INSTR-INDUCTION-SCHEME (st sym tm-- VA TM N)
(IF (ZEROP N)
T
(EVAL-INSTR-INDUCTION-SCHEME 'ST 'SYM (QUOTE (CDR TM))
(LIST (CONS 'ST (EVAL st VA
(tmi-fa TM)
N))
(CONS 'SYM (EVAL sym VA
(tmi-fa TM)
N))
(CONS 'TM (EVAL tm-- VA
(tmi-fa TM)
N)))
TM
(SUB1 N))))
(PROVE-LEMMA EVAL-INSTR (REWRITE)
(IMPLIES (AND (CNB (EV 'AL st VA (tmi-fa TM)
N))
(CNB (EV 'AL sym VA (tmi-fa TM)
N))
(CNB (EV 'AL tm-- VA (tmi-fa TM)
N)))
(EQUAL (EV 'AL (LIST 'INSTR st sym tm--)
VA
(tmi-fa TM)
N)
(INSTRN (EV 'AL st VA (tmi-fa TM)
N)
(EV 'AL sym VA (tmi-fa TM)
N)
(EV 'AL tm-- VA (tmi-fa TM)
N)
N)))
((INDUCT (EVAL-INSTR-INDUCTION-SCHEME st sym tm-- VA TM N))))
(PROVE-LEMMA EVAL-NEW-TAPE (REWRITE)
(IMPLIES (AND (CNB (EV 'AL op VA (tmi-fa TM)
N))
(CNB (EV 'AL tape VA (tmi-fa TM)
N)))
(EQUAL (EV 'AL (LIST 'NEW-TAPE op tape)
VA
(tmi-fa TM)
N)
(IF (ZEROP N)
(BTM)
(NEW-TAPE (EV 'AL op VA (tmi-fa TM)
N)
(EV 'AL tape VA (tmi-fa TM)
N))))))
(PROVE-LEMMA CNB-INSTRN (REWRITE)
(IMPLIES (AND (NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))))
(PROVE-LEMMA CNB-NEW-TAPE (REWRITE)
(IMPLIES (AND (CNB OP)
(CNB TAPE))
(CNB (NEW-TAPE OP TAPE))))
(TOGGLE NEW-TAPE-OFF NEW-TAPE T)
(DEFN TMIN (ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (BTMP (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N)))
(BTM)
(IF (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N))
(TMIN (CAR (CDR (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N))))
(NEW-TAPE (CAR (INSTRN ST (CAR (CDR TAPE))
TM
(SUB1 N)))
TAPE)
TM
(SUB1 N))
TAPE))))
(DEFN EVAL-TMI-INDUCTION-SCHEME (st tape tm-- VA TM N)
(IF (ZEROP N)
T
(EVAL-TMI-INDUCTION-SCHEME
(QUOTE (CAR (CDR (INSTR ST (CAR (CDR TAPE))
TM))))
(QUOTE (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE))
TM))
TAPE))
'TM
(LIST (CONS 'ST (EV 'AL st VA (tmi-fa TM)
N))
(CONS 'TAPE (EV 'AL tape VA (tmi-fa TM)
N))
(CONS 'TM (EV 'AL tm-- VA (tmi-fa TM)
N)))
TM
(SUB1 N))))
(PROVE-LEMMA EVAL-TMI (REWRITE)
(IMPLIES (AND (CNB (EV 'AL st VA (tmi-fa TM)
N))
(CNB (EV 'AL tape VA (tmi-fa TM)
N))
(CNB (EV 'AL tm-- VA (tmi-fa TM)
N)))
(EQUAL (EV 'AL (LIST 'TMI st tape tm--)
VA
(tmi-fa TM)
N)
(TMIN (EV 'AL st VA (tmi-fa TM)
N)
(EV 'AL tape VA (tmi-fa TM)
N)
(EV 'AL tm-- VA (tmi-fa TM)
N)
N)))
((INDUCT (EVAL-TMI-INDUCTION-SCHEME st tape tm-- VA TM N))))
(PROVE-LEMMA EVAL-tmi-x (REWRITE)
(IMPLIES (AND (CNB ST)
(CNB TAPE)
(CNB TM))
(EQUAL (EV 'AL (tmi-x ST TAPE)
NIL
(tmi-fa TM)
N)
(IF (ZEROP N)
(BTM)
(TMIN ST TAPE TM N)))))
(TOGGLE tmi-x-OFF tmi-x T)
(PROVE-LEMMA INSTRN-INSTR (REWRITE)
(IMPLIES (LESSP (LENGTH TM)
N)
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))))
(PROVE-LEMMA NBTMP-INSTR (REWRITE)
(IMPLIES (TURING-MACHINE TM)
(NOT (BTMP (INSTR ST SYM TM)))))
(PROVE-LEMMA INSTRN-NON-F (REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(INSTRN ST SYM TM N)))
(PROVE-LEMMA TMIN-BTM (REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(EQUAL (TMIN ST TAPE TM N)
(BTM))))
(PROVE-LEMMA TMIN-TMI (REWRITE)
(IMPLIES (TURING-MACHINE TM)
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM
(PLUS K (ADD1 (LENGTH TM)))))))
(PROVE-LEMMA SYMBOL-CNB (REWRITE)
(IMPLIES (SYMBOL SYM)
(CNB SYM)))
(TOGGLE SYMBOL-OFF SYMBOL T)
(PROVE-LEMMA HALF-TAPE-CNB (REWRITE)
(IMPLIES (HALF-TAPE X)
(CNB X)))
(PROVE-LEMMA TAPE-CNB (REWRITE)
(IMPLIES (TAPE X)
(CNB X)))
(TOGGLE TAPE-OFF TAPE T)
(PROVE-LEMMA OPERATION-CNB (REWRITE)
(IMPLIES (OPERATION OP)
(CNB OP)))
(TOGGLE OPERATION-OFF OPERATION T)
(PROVE-LEMMA TURING-MACHINE-CNB (REWRITE)
(IMPLIES (TURING-MACHINE TM)
(CNB TM)))
(TOGGLE TURING-MACHINE-OFF TURING-MACHINE T)
(PROVE-LEMMA TURING-COMPLETENESS-OF-LISP NIL
(IMPLIES (AND (STATE ST)
(TAPE TAPE)
(TURING-MACHINE TM))
(AND (IMPLIES (NOT (BTMP (EVAL (tmi-x ST TAPE)
NIL
(tmi-fa TM)
N)))
(NOT (BTMP (TMI ST TAPE TM
(tmi-k ST TAPE TM N)))))
(IMPLIES (NOT (BTMP (TMI ST TAPE TM K)))
(EQUAL (TMI ST TAPE TM K)
(EVAL (tmi-x ST TAPE)
NIL
(tmi-fa TM)
(tmi-n ST TAPE TM K))))))
NIL))
NIL "TMI")
;;; "ZTAK"
(PROVEALL
'((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
(ADD-SHELL ZN NIL ZNP ((POS (ONE-OF NUMBERP)
ZERO)
(NEG (ONE-OF NUMBERP)
ZERO)))
(DEFN ZLESSP (X Y)
(LESSP (PLUS (POS X)
(NEG Y))
(PLUS (NEG X)
(POS Y))))
(DEFN ZLESSEQP (X Y)
(NOT (ZLESSP Y X)))
(DEFN ZMAX (X Y)
(IF (ZLESSP X Y)
Y X))
(DEFN ZMIN (X Y)
(IF (ZLESSP X Y)
X Y))
(DEFN ZSUB1 (X)
(ZN (POS X)
(ADD1 (NEG X))))
(DEFN PZDIFFERENCE (X Y)
(DIFFERENCE (PLUS (POS X)
(NEG Y))
(PLUS (NEG X)
(POS Y))))
(DEFN M1 (X Y Z)
(IF (ZLESSEQP X Y)
0 1))
(DEFN M2 (X Y Z)
(PZDIFFERENCE (ZMAX X (ZMAX Y Z))
(ZMIN X (ZMIN Y Z))))
(DEFN M3 (X Y Z)
(PZDIFFERENCE X (ZMIN X (ZMIN Y Z))))
(DEFN TAK0 (X Y Z)
(IF (ZLESSEQP X Y)
Y
(IF (ZLESSEQP Y Z)
Z X)))
(DEFN M (X Y Z)
(CONS (M1 X Y Z)
(CONS (M2 X Y Z)
(CONS (M3 X Y Z)
NIL))))
(PROVE-LEMMA TAK0-SATISFIES-TAK-EQUATION NIL
(EQUAL (TAK0 X Y Z)
(IF (ZLESSEQP X Y)
Y
(TAK0 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y)))))
(PROVE-LEMMA M1-LESSEQP-0 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))))))
(PROVE-LEMMA M1-LESSEQP-1 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 X)
Y Z)))))
(PROVE-LEMMA M1-LESSEQP-2 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 Y)
Z X)))))
(PROVE-LEMMA M1-LESSEQP-3 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M1 X Y Z)
(M1 (ZSUB1 Z)
X Y)))))
(PROVE-LEMMA M2-LESSEQP-0 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M2 X Y Z)
(M2 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))))))
(PROVE-LEMMA M2-LESSEQP-1 (REWRITE)
(IMPLIES (NOT (ZLESSEQP X Y))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 X)
Y Z)))))
(PROVE-LEMMA M2-LESSEQP-2 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Y)
Z X)
(M1 X Y Z)))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 Y)
Z X)))))
(PROVE-LEMMA M2-LESSEQP-3 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Z)
X Y)
(M1 X Y Z)))
(NOT (LESSP (M2 X Y Z)
(M2 (ZSUB1 Z)
X Y)))))
(PROVE-LEMMA M3-LESSP-0 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M1 X Y Z)))
(LESSP (M3 (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-1 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 X)
Y Z)
(M1 X Y Z)))
(LESSP (M3 (ZSUB1 X)
Y Z)
(M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-2 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Y)
Z X)
(M1 X Y Z)))
(LESSP (M3 (ZSUB1 Y)
Z X)
(M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-3 (REWRITE)
(IMPLIES (AND (NOT (ZLESSEQP X Y))
(EQUAL (M1 (ZSUB1 Z)
X Y)
(M1 X Y Z)))
(LESSP (M2 (ZSUB1 Z)
X Y)
(M2 X Y Z))))
(DISABLE ZLESSP)
(DISABLE M1)
(DISABLE M2)
(DISABLE M3)
(DISABLE TAK0)
(DISABLE ZSUB1)
(PROVE-LEMMA M-GOES-DOWN-1 NIL
(IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 X)
Y Z)
(M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-2 NIL
(IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 Y)
Z X)
(M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-3 NIL
(IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (ZSUB1 Z)
X Y)
(M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-0 NIL
(IMPLIES (NOT (ZLESSEQP X Y))
(LEX3 (M (TAK0 (ZSUB1 X)
Y Z)
(TAK0 (ZSUB1 Y)
Z X)
(TAK0 (ZSUB1 Z)
X Y))
(M X Y Z)))
NIL))
NIL "ZTAK")